A toy dependently typed language implementation in C++.
- Base on Martin-Löf's intuitionistic type theory and Normalization by Evaluation.
- Support dependent function type, non-cumulative Russell style universes.
- Support universe level polymorphism.
- Pretty Printer.
- Module System
- Unit Test
- Evaluation Optimization
Dependencies:
- clang, cmake, and make
- flex and bison
mkdir build
cd build
cmake ..
make
bin/bin /path/to/input