minitt 0.1.9

Mini-TT, a dependently-typed lambda calculus, implementated in Rust
Documentation 
1
2
3
4
5
6
7
8

let f1 : U = 1;
-- U is universe, the type of types.
-- 1 is the "one" type, which have one instance.

let f2 : 1 = 0;
-- .. and 0 is the instance of 1.

-- Unfortunately comments are not allowed at the beginning of a file :(