Dependently-Typed Lambda Experiment

A dependently typed lambda calulus, implemented in Jetbrains MPS.

Acknowledgment

This project is based on Andrej Bauer's excellent tutorial "how to implement dependent type theory" (part I).

Remarks

I followed through part I of the tutorial (which means that normalization is done by substitution), then added data types.