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)