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
23
24
25
26
27
28
29
30
31

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

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

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

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

let elimBool
  : \Pi c : bool → Type
  . \Pi _ : c False
  . \Pi _ : c True
  . \Pi b : bool
  . c b

  = λ c . λ h0 . λ h1 . split
  { True => h1
  | False => h0
  };