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
-- A pair whose type is a sigma type
let pair: \Sigma a: 1. 1 = 0, 0;

-- Projections
let fst: 1 = pair.1;
let snd: 1 = pair.2;

-- Vanilla Mini-TT does not support this (IIRC).
let new_feature: 1 = (0, 0).2;

-- Have to add a parenthesis between, because I didn't spend much time
-- on the parser.
let complicated: 1 = (((0, 0), (0, 0).2).1).2;