Library FinSet.FinSet
- Low level interface
- Quantifiers
- Set-theoretical operations
- Extensionality
- Standard notations
- Algebraic properties
- Categorical combinators
- Notations
Library FinSet.Quotients.Quotient
Library FinSet.Quotients.UList
Library FinSet.Quotients.Countable
Library FinSet.Quotients.Retract
Library FinSet.Lib.ListSet
- Inductive member predicate
- Decidable quantifiers on lists members
- Set-like decidable relations on lists
- List without duplicates
Library FinSet.Lib.DProp
Library FinSet.Lib.CEExt
This page has been generated by coqdoc