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

-- Pi, lambda
let a: Πx: bool. bool = λx. x;

-- Multiplication, both OK
let b: bool ✖ bool × bool = (1, 1, 1);

-- Sigma
let c: Σx: bool. bool = bla;

-- Arrows
let d: bool → bool = split
 { True _ ⇒ False 0
 | False _ ⇒ True 0
 };