~/bend-docscommunity

proofs/containers/deque/state.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/state.bend as State

3 imports
import Base
import ../../../spec/lib/common.bend as SC
import ../../../src/containers/deque.bend as DQ

Types

type Shadow source · line 10 · raw

@-T:Data -> Data

Definitions

def initial source · line 13 · raw

@-T:Data -> Shadow<T>

def real source · line 16 · raw

@-T:Data -> @sh:Shadow<T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.Deque<T>

def model source · line 21 · raw

@-T:Data -> @sh:Shadow<T> -> List<&2, T>

def unreal source · line 26 · raw

@-T:Data -> @d:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.Deque<T> -> Shadow<T>

def unreal_real source · line 30 · raw

@-T:Data -> @+sh:Shadow<T> -> {unreal(T, real(T, sh)) == sh : Shadow<T>}

def real_inj source · line 36 · raw

@-T:Data -> @+a:Shadow<T> -> @+b:Shadow<T> -> @+e:{real(T, a) == real(T, b) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.Deque<T>} -> {a == b : Shadow<T>}

a deque determines its shadow