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
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

use std::rc::Rc;

use crate::ast::*;

/// `NRho` in Mini-TT, normal form telescopes (contexts).
pub type NormalTelescope = Rc<GenericTelescope<NormalExpression>>;

/// `NSClos` in Mini-TT, normal form closures.
pub type NormalDeepClosure = GenericCaseTree<NormalExpression>;

/// `NNeut` in Mini-TT, normal form neutral values.
pub type NormalNeutral = GenericNeutral<NormalExpression>;

/// `NExp` in Mini-TT, normal form expressions.<br/>
/// Deriving `Eq` so we can do comparison.
#[derive(Debug, Clone, Eq, PartialEq)]
pub enum NormalExpression {
    Lambda(u32, Box<Self>),
    Pair(Box<Self>, Box<Self>),
    Unit,
    One,
    Type,
    Pi(Box<Self>, u32, Box<Self>),
    Sigma(Box<Self>, u32, Box<Self>),
    Constructor(String, Box<Self>),
    Split(NormalDeepClosure),
    Sum(NormalDeepClosure),
    Neutral(NormalNeutral),
}