364 B


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)