Library FSets.MSetFullAVL
- MSetFullAVL : some complements to MSetAVL
- AVL trees
- Automation and dedicated tactics
- AVL trees have indeed logarithmic depth
- The AVL invariant is preserved by set operations
- Encapsulation
- ocaml_union, an union faithful to the original ocaml code
- ocaml_subset, a subset faithful to the original ocaml code
- Equality test
Library FSets.MSetAVL_test
Library FSets.demo_msets
- Ordered types
- An example of OrderedType :
- Let's now build some sets of Z integers ...
- union
- Some sets of sets ...
- Some more intense tests.
- Proving with FSets : the facts/properties functors
- The Weak Sets and Maps
Library FSets.demo
- Ordered types
- An example of OrderedType :
- Let's now build some sets of Z integers ...
- union
- Some sets of sets ...
- Some more intense tests.
- Proving with FSets : the facts/properties functors
- What about maps ? it's the same !
- The Weak Sets and Maps
Library FSets.MultiSetsEq
Library FSets.MultiSets
Library FSets.FSetListEq
Library FSets.FMapListEq
Library FSets.PowerSet
Library FSets.MapFunction
Library FSets.UsualFacts
Library FSets.PrecedenceGraph.PrecedenceGraph
Library FSets.extract
Library FSets.FSetAVL_test
Library FSets.FSetAVL_prog
- Trees
- Occurrence in a tree
- Binary search trees
- AVL trees
- Some shortcuts.
- Empty set
- Emptyness test
- Appartness
- Singleton set
- Helper functions
- Insertion
- Join
- Extraction of minimum element
- Merging two trees
- Deletion
- Minimum element
- Maximum element
- Any element
- Concatenation
- Splitting
- Intersection
- Difference
- Elements
- Filter
- Partition
- Fold
- Cardinal
- Union
- Subset
- Comparison
- A new comparison algorithm suggested by Xavier Leroy
- Equality test
- Encapsulation
Library FSets.FSetAVL_dep
- Trees
- Occurrence in a tree
- Binary search trees
- AVL trees
- Sets as AVL trees
- Logical appartness
- Empty set
- Emptyness test
- Appartness
- Singleton set
- Helper functions
- Insertion
- Join
- Extraction of minimum and maximum element
- Merging two trees
- Deletion
- Minimum element
- Maximum element
- Any element
- Concatenation
- Splitting
- Intersection
- Difference
- Elements
- Cardinal
- Union
- Filter
- Partition
- Subset
- Fold
- Comparison
- Equality test
Library FSets.FSetRBT
- Red-black trees
- Occurrence in a tree
- Binary search trees
- Balanced red-black trees
- Sets as red-black trees
- Logical appartness
- Empty set
- Emptyness test
- Appartness
- Singleton set
- Insertion
- Deletion
- From lists to red-black trees
- Elements
- Isomorphism with FSetList
- Union
- Intersection
- Difference
- Equality test
- Inclusion test
- Fold
- Cardinal
- Filter
- Minimum element
- Maximum element
- Any element
- Comparison
Library FSets.FSetFullAVL
- FSetFullAVL : some complements to FSetAVL
- AVL trees
- Automation and dedicated tactics
- Results about avl
- ocaml_union, an union faithful to the original ocaml code
- ocaml_subset, a subset faithful to the original ocaml code
- Equality test
- Encapsulation
Library FSets.FSetAVL0
- FSetAVL : Implementation of FSetInterface via AVL trees
- Raw
- Trees
- Basic functions on trees: height and cardinal
- Empty Set
- Emptyness test
- Appartness
- Singleton set
- Helper functions
- Insertion
- Join
- Extraction of minimum element
- Merging two trees
- Deletion
- Minimum element
- Maximum element
- Any element
- Concatenation
- Splitting
- Intersection
- Difference
- Union
- Elements
- Filter
- Partition
- for_all and ∃
- Fold
- Subset
- A new comparison algorithm suggested by Xavier Leroy
- Equality test
- Invariants
- Some shortcuts
- Correctness proofs, isolated in a sub-module
- Automation and dedicated tactics
- Basic results about In, lt_tree, gt_tree, height
- Inductions principles
- Empty set
- Emptyness test
- Appartness
- Singleton set
- Helper functions
- Insertion
- Join
- Extraction of minimum element
- Merging two trees
- Deletion
- Minimum element
- Maximum element
- Any element
- Concatenation
- Splitting
- Intersection
- Difference
- Union
- Elements
- Filter
- Partition
- for_all and ∃
- Fold
- Subset
- Comparison
- A new comparison algorithm suggested by Xavier Leroy
- Equality test
- Encapsulation