Controlling computation in type theory, locally

Utility

General tactics, lemmas and notations are defined in Util.

Syntax

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.

Type Theory and its meta-theory