Encoding Indexed Inductive Defintions using the Intensional Identity Type
Formalisation
Logic/Base.agda
Logic/ChainReasoning.agda
LF.agda
Identity.agda
DefinitionalEquality.agda
IID.agda
IIDr.agda
IID-Proof-Setup.agda
IID-Proof.agda
All files are UTF-8 encoded.