This is a simple implementation of the calculus of constructions.
This implementation is a normalization by evaluation type checker with bidirectional type checking, based heavily on the tutorial by David Christensen found here.
- This typechecker currently has type in type, and is inconsistent as a formal logic. I have not decided if I care about that in the long term, as I want this to be a programming language over a theorem prover.