Library PropiL
- Formulas and contexts
- Generic Entailment Relations
- Intuitionistic Gentzen System
- Intuitionistic Natural Deduction System
- Equivalence of Ni and Gi
- Intuitionistic Hilbert System Hi
- Intuitionistic Tableaux (Fitting's System)
- Decidability of Intuitionistic Gentzen
Library PropcL
- Classical Natural Deduction
- Boolean Entailment
- Refutation predicates
- Decision trees
- Refutation lemma
- Decidability of classical ND entailment
- Agreement of classical ND entailment with boolean entailment
- Classical Gentzen system
- Equivalence between GK3c and Nc
- Cut elimination in GK3c
- Agreement of classical Gentzen with boolean entailment
- Classical Hilbert System Hc
Library Base
- Base Library for ICL
- De Morgan laws
- Size recursion
- Iteration
- Decidability
- 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
- Finite closure iteration
- Deprecated names, defined for backward compatibilitly
This page has been generated by coqdoc