~/bend-docscommunity

proofs/containers/doubly_linked_list/ok.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/ok.bend as Ok

5 imports
import Base
import ../../lib/logic.bend as L
import ../../../spec/containers/doubly_linked_list.bend as S
import ../../../src/containers/doubly_linked_list.bend as D
import ./state.bend as ST

Templates

template POK source · line 11 · raw

@-T:Data -> @-X:Data -> @spec:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, X) -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, X) -> Type

template pok_eq source · line 15 · raw

@-T:Data -> @-X:Data -> @-spec:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, X) -> @-spec2:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, X) -> @-r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, X) -> @-r2:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, X) -> @+es:{spec == spec2 : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, X)} -> @+er:{r == r2 : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, X)} -> @p:POK(T, X, spec2, r2) -> POK(T, X, spec, r)

both results rewritten