dtt
A simple dependent type theory which can be used to verify very simple
theorems.
dtt
does not have:
- recursive definitions (TODO: a totality checker so we can allow this)
- Σ types
- a standard library
dtt
does have:
- Π types
- unification-based type equality
- pattern matching
- inductive data types (use postulations if possible)