minitt 0.4.3

Mini-TT, a dependently-typed lambda calculus, extended and (re)implemented in Rust
Documentation 
1
2
3
4
5
6

let pair2: \Sigma a: Type1. Type1 = Type0, Type0;
let pair1: \Sigma a: Type0. Type0 = 1, 1;

rec rec_sum: Type2 = Sum { Nil Type1 | Cons rec_sum };

rec s: Type = Sum { Nil | Cons s };