~/bend-docscommunity

proofs/containers/deque/stepok.bend checks

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

5 imports
import Base
import ../../../spec/containers/deque.bend as S
import ../../../src/containers/deque.bend as DQ
import ../../../src/containers/types/deque.bend as E
import ./state.bend as ST

Templates

template StepOK source · line 11 · raw

@-T:Data -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Op<T> -> Type

template mk source · line 14 · raw

@-T:Data -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Op<T> -> @sh2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> @o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Obs<T> -> @e1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, sh), op) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(T, sh2), o) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.Deque<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Obs<T>)} -> @e2:{(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh2), o) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/deque.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(T, sh), op) : Pair(List<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Obs<T>)} -> StepOK(T, sh, op)