minitt 0.1.9

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

let bool: U = sum { True 1 | False 1 };
let unit: U = sum { TT 1 };
-- 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 0
 | False _ => 0
 };
-- Return things that are of different types.