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

let maybe: U -> U = \lambda t. sum { Just t | Nothing 1 };

let the: \Pi t: U. (t -> t) = \lambda _. \lambda a. a;

let unwrap_type (t : U): (maybe t) -> U = split
  { Just _ => t
  | Nothing _ => 1
  };

-- let unwrap (t : U) (mt: maybe t): unwrap_type t mt = split
--   { Just a => a
--   | Nothing _ => 0
--   };