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

let bool: U = sum { True 1 | False 1 };
-- Each constructor have only one argument
-- Capitalized names are constructors so constructor calls are lexically
-- recognizable

let not: bool -> bool = split
 { True  n => False n
 | False n => True  n
 };
-- Pattern matching

let boolean_id: bool -> bool = \lambda n . n;
-- Simple functions can be defined with lambdas

let and: bool -> bool -> bool = split
 { True n => boolean_id
 | False n => \lambda _. False n
 };
-- Nested functions