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::syntax::*;
pub type NormalTelescope = Rc<GenericTelescope<NormalExpression>>;
pub type NormalDeepClosure = GenericCaseTree<NormalExpression>;
pub type NormalNeutral = GenericNeutral<NormalExpression>;
#[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),
}