Library Base
- Base Library for ICL
- Iteration
- Decidability
- Lists
- Filter
- Element removal
- Duplicate-free lists
- Cardinality
- Power lists
- Finite closure iteration
Library ARS
Library LexSizeInduction
Library UnifConfl
- Uniform Confluence
- Uniform Diamond
- Proof of Equivalence
- Characterization of Niehren
- Irreducibility
- Uniform Confluence and Irreducible Terms
Library L
- Syntax of the weak call-by-value lambda calculus
- Notation using binders
- Important terms
- Substitution
- Important definitions
- Size of terms
- Reduction
- Properties of the reduction relation
- Equivalence
- Definition of convergence
- Eta expansion
- Useful lemmas
Library SKv
- Syntax of SKv
- Semantics of SKv
- Decidability of Basic Predicates
- Identity Combinator
- Compatibility Laws
- Irreducibility
- Closedness
- Uniform Confluence
- Misc
Library SKvTactics
Library SKvAbstraction
Library LC
- Syntax of L with Closures
- Semantics
- Uniform Confluence
- Compatibility Laws
- Connecting L and LC
- Completeness
- Simulation Lemma
Library LC_eval
This page has been generated by coqdoc