Library stdpp.base
- Enable implicit generalization.
- Tweak program
- Sealing off definitions
- Non-backtracking type classes
- Typeclass opaque definitions
- Equality
- Type classes
- Logic
- Common data types
- Operations on sets
- Monadic operations
- Operations on maps
- Axiomatization of sets
- Miscellaneous
- Notations for lattices.
Library stdpp.tactics
Library stdpp.option
Library stdpp.fin_map_dom
Library stdpp.boolset
Library stdpp.fin_maps
- Axiomatization of finite maps
- Derived operations
- Theorems
- Setoids
- General properties
- Properties of the partial_alter operation
- Properties of the alter operation
- Properties of the delete operation
- Properties of the insert operation
- Properties of the singleton maps
- Properties of the map operations
- Properties of conversion to lists
- Properties of the size operation
- Properties of conversion from sets
- Induction principles
- The fold operation
- The filter operation
- Properties of the map_Forall predicate
- Properties of the merge operation
- Properties on the map_relation relation
- Properties on the disjoint maps
- Properties of the union_with operation
- Properties of the union operation
- Properties of the union_list operation
- Properties of the folding the delete function
- Properties on disjointness of conversion to lists
- Properties of the intersection_with operation
- Properties of the intersection operation
- Properties of the difference_with operation
- Properties of the difference operation
- The seq operation
- Tactics
Library stdpp.fin
Library stdpp.vector
Library stdpp.pmap
Library stdpp.stringmap
Library stdpp.fin_sets
- The elements operation
- The size operation
- Induction principles
- The set_fold operation
- Minimal elements
- Filter
- Map
- Decision procedures
Library stdpp.mapset
Library stdpp.proof_irrel
Library stdpp.hashset
Library stdpp.pretty
Library stdpp.countable
Library stdpp.orders
Library stdpp.natmap
Library stdpp.strings
Library stdpp.relations
Library stdpp.sets
- Setoids
- Setoids
- Tactics
- Sets with ∪, ∅ and {[_]}
- Sets with ∪, ∩, ∖, ∅ and {[_]}
- Conversion of option and list
- Guard
- Quantifiers
- Properties of implementations of sets that form a monad
Library stdpp.listset
Library stdpp.streams
Library stdpp.gmap
- The data structure
- Operations on the data structure
- Instantiation of the finite map interface
- Curry and uncurry
- Finite sets
Library stdpp.gmultiset
Library stdpp.prelude
Library stdpp.listset_nodup
Library stdpp.finite
Library stdpp.numbers
- Notations and properties of nat
- Notations and properties of positive
- Notations and properties of N
- Notations and properties of Z
- Injectivity of casts
- Notations and properties of Qc
- Positive rationals
Library stdpp.nmap
Library stdpp.zmap
Library stdpp.coPset
- The tree data structure
- Packed together + set operations
- Top
- Finite sets
- Pick element from infinite sets
- Conversion to psets
- Conversion from psets
- Conversion to and from gsets of positives
- Domain of finite maps
- Suffix sets
- Splitting of infinite sets
Library stdpp.lexico
Library stdpp.propset
Library stdpp.decidable
Library stdpp.list
- Definitions
- Basic tactics on lists
- General theorems
- Properties of the elem_of predicate
- Properties of the NoDup predicate
- Set operations on lists
- Properties of the omap function
- Properties of the reverse function
- Properties of the last function
- Properties of the take function
- Properties of the drop function
- Properties of the replicate function
- Properties of the resize function
- Properties of the reshape function
- Properties of sublist_lookup and sublist_alter
- Properties of the imap function
- Properties of the mask function
- Properties of the seq function
- Properties of the Permutation predicate
- Properties of the filter function
- Properties of the prefix and suffix predicates
- Properties of the sublist predicate
- Properties of included
- Properties of the Forall and Exists predicate
- Properties of the Forall2 predicate
- Properties of the find function
- Properties of the monadic operations
- Relection over lists
- Tactics
Library stdpp.functions
Library stdpp.hlist
Library stdpp.sorting
Library stdpp.infinite
Library stdpp.nat_cancel
Library stdpp.namespaces
Library stdpp.telescopes
Library stdpp.binders
This page has been generated by coqdoc