A dependent type theory

hydraz 954c02672b Add some context to type errors 1 year ago
src 954c02672b Add some context to type errors 1 year ago
.gitignore 24900ea148 Initial commit 1 year ago
ChangeLog.md 24900ea148 Initial commit 1 year ago
LICENSE 24900ea148 Initial commit 1 year ago
README.md 6824d1cb4a Add some very rudimentary elaboration support 1 year ago
Setup.hs 24900ea148 Initial commit 1 year ago
default.nix 24900ea148 Initial commit 1 year ago
dtt.cabal 357b4802ce Fix most warnings. 1 year ago
example.dtt ccced2c25d Make example even more complex 1 year ago

README.md

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)