minitt 0.2.2

Mini-TT, a dependently-typed lambda calculus, extended and implementated in Rust
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

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

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

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