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

rec nat : Type = Sum { Zero | Suc nat };
-- Inductive definition of nat

let one : nat = Zero;

let two : nat = Suc one;

let test_case_split: nat -> Type = 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
 | Suc n => n
 };