minitt 0.2.2

Mini-TT, a dependently-typed lambda calculus, extended and implementated in Rust
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13

let pair: \Sigma a: 1. 1 = 0, 0;
-- A pair whose type is a sigma type

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

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

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