29 lines
501 B
Standard ML
29 lines
501 B
Standard ML
nat : Type
|
|
PTm(VarPTm) : Type
|
|
Tm(VarTm) : Type
|
|
PTag : Type
|
|
TTag : Type
|
|
bool : Type
|
|
|
|
PL : PTag
|
|
PR : PTag
|
|
TPi : TTag
|
|
TSig : TTag
|
|
|
|
PAbs : (bind PTm in PTm) -> PTm
|
|
PApp : PTm -> PTm -> PTm
|
|
PPair : PTm -> PTm -> PTm
|
|
PProj : PTag -> PTm -> PTm
|
|
PConst : TTag -> PTm
|
|
PUniv : nat -> PTm
|
|
PBot : PTm
|
|
|
|
Abs : (bind Tm in Tm) -> Tm
|
|
App : Tm -> Tm -> Tm
|
|
Pair : Tm -> Tm -> Tm
|
|
Proj : PTag -> Tm -> Tm
|
|
TBind : TTag -> Tm -> (bind Tm in Tm) -> Tm
|
|
Univ : nat -> Tm
|
|
BVal : bool -> Tm
|
|
Bool : Tm
|
|
If : Tm -> Tm -> Tm -> Tm
|