## Library stdpp.options

## 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
- Notations for lattices.
- Axiomatization of sets
- Miscellaneous

## 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
- 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 conversion to lists that depend on ∪ and ##ₘ
- Properties of the intersection_with operation
- Properties of the intersection operation
- Properties of the difference_with operation
- Properties of the difference operation
- Misc properties about the order
- Setoids
- The map_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.well_founded

## Library stdpp.relations

## Library stdpp.sets

- Setoids
- Setoids
- Tactics
- Sets with ∪, ∅ and {[_]}
- Sets with ∪, ∩, ∖, ∅ and {[_]}
- Sets with ∪, ∩, ∖, ∅, {[_]}, and ⊤
- Conversion of option and list
- Finite types to sets.
- 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
- Helper for working with accessing lists with wrap-around

## Library stdpp.nmap

## Library stdpp.zmap

## Library stdpp.coPset

- The tree data structure
- Packed together + set operations
- Finite sets
- Pick element from infinite sets
- Conversion to psets
- Conversion from psets
- Conversion to and from gsets of positives
- Infinite sets
- Domain of finite maps
- Suffix sets
- Splitting of infinite sets

## Library stdpp.coGset

- Pick elements from infinite sets
- Conversion to and from gset
- Conversion to coPset
- Inefficient conversion to arbitrary sets with a top element
- Domain of finite maps

## Library stdpp.lexico

## Library stdpp.propset

## Library stdpp.decidable

## Library stdpp.list

- Definitions
- Basic tactics on lists
- General theorems
- Properties of the reverse function
- Properties of the elem_of predicate
- Properties of the NoDup predicate
- Set operations on lists
- Properties of the last function
- Properties of the head function
- Properties of the take function
- Properties of the drop function
- Properties of the replicate function
- Properties of the resize function
- Properties of the rotate function
- Properties of the rotate_take function
- Properties of the reshape function
- Properties of sublist_lookup and sublist_alter
- Properties of the mask 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.list_numbers

## 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