proofs/PROOF.bend

bend-collections-laws-containers@1.0.0.0 · 18 lines · 0 definitions

1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/proof.bend as IntrusiveList
3import bend-collections-laws-containers@1.0.0.0/proofs/containers/dlist_iterator/proof.bend as IteratorComponents
4import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/components.bend as TreeMapComponents
5import bend-collections-laws-containers@1.0.0.0/proofs/END_TO_END.bend as End
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/public_trace.bend as LruTrace
7import bend-collections-laws-containers@1.0.0.0/proofs/math/proof.bend as Math
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/proof.bend as HashTable
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/proof.bend as Lru
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/proof.bend as Dll
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/proof.bend as TreeMap
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitlist/proof.bend as Bitlist
13
14# Root gate. Checks END_TO_END.bend (and through it every proofs/<id>.bend
15# entry), the retained LRU's trace refinement (lib/lemmas/proofs/public_trace),
16# the math library, the refinements of the hash map, the LRU cache, the doubly
17# linked list, the indexed TreeMap and the bit list, and the TreeMap's
18# component laws.