Library BA.External
- Proofs and definitions obtained from external sources
- De Morgan laws
- Lists
- Decidability laws for lists
- Membership
- Disjointness
- Inclusion
- Setoid rewriting with list inclusion and list equivalence
- Equivalence
- Filter
- Element removal
- Cardinality
- Duplicate-free lists
- Power lists
Library BA.BasicDefinitions
- Basic definitions of decidablility and Functions
- Definition of useful tactics
- Injectivity and surjectivity
- Pure predicates
- Proofs about equality
- Decidablility of equality: Instance declarations
- Functions creating an eqType from a type or a value
- Definitions of corresponding eqTypes
- Useful notations for cross product and option eqTypes
- toeqType produces canonical instances
- Definition of useful functions
- Basic lemmas about functions
- Cardinality Lemmas for lists
- Various helpful Lemmas
Library BA.FinTypes
- Definition of finite Types
- Properties of decidable Propositions
- Completeness Lemmas for lists of basic types
- Canonical structures declarations for finTypes of base types
- Correctness of finTypes for basic types
- Tests and Examples
- Examples depending on type classes
- Definition of sum Type as finType
- Dupfreeness
- Definition of vectors (extensional/ set theoretic functions)
- Proofs about Cardinality
- Dependent pairs
- Subtypes
- finTypes from Lists
- Finite Closure Iteration