minitt-rs

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.

Mini-TT Paper

Features

• [X] Everything that the Haskell implementation has
  • [ ] Use Vec for telescope instead of functional immutable list
  • [X] Use BTreeMap for branch/case tree so we become flexible on case order
  • [X] Support inferring type of a pair
• [ ] Parser as a cargo feature
• [X] AST pretty-printer as a cargo feature