minitt 0.4.3

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

const bool = Sum { True | False };

const myTrue = True;
-- Sum subtyping
let check: bool = myTrue;

rec nat: Type1 = Sum { Zero | Suc nat };

const myZero = Zero;
-- Yes, minitt supports shadowing
let check: nat = myZero;