Rust implementation of Mini-TT, a simple dependently-typed lambda calculus. It can be used as a core language for complicated dependently-typed programming languages, or used for testing the correctness of translation algorithms.
I'm trying my best to use complete and meaningful namings. I'm also doing a general clean-up of the Haskell implementation and comment the functions with their counterparts' names in the Haskell implementation so people don't get confused when they read the paper while reading this implementation.
- Initial version: just
cloneand simulate the Haskell implementation
- Update: use mutable
BTreeMapfor telescopes instead of functional immutable lists to improve efficiency
- Update: replace the use of
Boxto the use of
- Update: add a parser, enabled with