General tactics, lemmas and notations are defined in Util.
We define a common syntax for both MLTT and its extension. BasicAST contains the notion of references (for variables). autosubst/AST.sig
is used to generate the autosubst/AST module. autosubst/core, autosubst/unscoped and autosubst/SubstNotations contain the Autosubst library and some notations. autosubst/RAsimpl contains implementation for the rasimpl
tactic, a faster substitution simplification tactic, whereas autosubst/AST_rasimpl provide the corresponding instance for our syntax.
Env defines global, interface, and local environments.
Inst defines operations to instantiate an interface.
Module | Description |
---|---|
GScope | Notion of global scope |
IScope | Interface scoping |
Typing | Conversion and typing judgements |
BasicMetaTheory | Meta-theory like substitution and validity |
Inversion | Inversion of typing lemmas |
Inlining | Inlining and conservativity results |
Confluence | Generic results about confluence |
Reduction | Reduction, injectvity of Π, subject reduction |
Pattern | Proof-of-concept confluence proof |