laws_containers.bend
bend-collections-laws-containers@1.0.0.0 · 31 lines · 0 definitions
1import Base
2
3# bend-collections-laws-containers: the proved laws of bend-collections' containers, the shared proof library and the whole-library roots (END_TO_END, PROOF).
4# Importing this file checks every proof root below; see docs/*_CONTRACTS.md
5# for what each clause states and what is not proved. Part of
6# bend-collections-laws (laws.bend imports all three parts by name).
7
8import bend-collections-laws-containers@1.0.0.0/proofs/END_TO_END.bend as ENDTOEND
9import bend-collections-laws-containers@1.0.0.0/proofs/PROOF.bend as PROOF
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/components.bend as ContainersBalancedSearchTreeComponents
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/proof.bend as ContainersBalancedSearchTreeProof
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/range.bend as ContainersBalancedSearchTreeRange
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitlist/proof.bend as ContainersBitlistProof
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/proof.bend as ContainersBitsetProof
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/proof.bend as ContainersDequeProof
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/dlist_iterator/proof.bend as ContainersDlistIteratorProof
17import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/direct_laws.bend as ContainersDoublyLinkedListDirectLaws
18import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/proof.bend as ContainersDoublyLinkedListProof
19import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/proof.bend as ContainersDynamicArrayProof
20import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/proof.bend as ContainersHashTableProof
21import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/proof.bend as ContainersIntrusiveDoublyLinkedListProof
22import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/proof.bend as ContainersLruProof
23import bend-collections-laws-containers@1.0.0.0/proofs/containers/priority_queue/proof.bend as ContainersPriorityQueueProof
24import bend-collections-laws-containers@1.0.0.0/proofs/containers/simple_queue/proof.bend as ContainersSimpleQueueProof
25import bend-collections-laws-containers@1.0.0.0/proofs/containers/stack/components.bend as ContainersStackComponents
26import bend-collections-laws-containers@1.0.0.0/proofs/lib/array2.bend as LibArray2
27import bend-collections-laws-containers@1.0.0.0/proofs/lib/flat.bend as LibFlat
28import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/public_trace.bend as LibLemmasPublicTrace
29import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32seq.bend as LibU32seq
30import bend-collections-laws-containers@1.0.0.0/proofs/lib/vec.bend as LibVec
31import bend-collections-laws-containers@1.0.0.0/spec/containers/balanced_search_tree/recursive.bend as SpecContainersBalancedSearchTreeRecursive