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
12
13
14
15

-- A 2 type and a 1 type
const bool = Sum { True | False };
const unit = Sum { TT };

-- By `function.minitt` of course I mean dependent functions :)
let return_type: bool -> Type = split
 { True => unit
 | False => 1
 };

-- Return things that are of different types.
let function: \Pi b: bool. return_type b = split
 { True => TT
 | False => 0
 };