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
16
17
18
19
20
21
22

rec nat : U = sum { Zero 1 | Suc nat };
-- Inductive definition of nat

let one : nat = Zero 0;

let two : nat = Suc one;

let test_case_split: nat -> U = split
 { Zero _ => 1
 | Suc  _ => 1
 };

let zero_anyway: \Pi n: nat. test_case_split n = split
 { Zero _ => 0
 | Suc  _ => 0
 };
-- Dependent function!

let pred: \Pi n: nat. nat = split
 { Zero _ => Zero 0
 | Suc  n => n
 };