18 lines
268 B
Standard ML
18 lines
268 B
Standard ML
Tm(VarTm) : Type
|
|
Ty : Type
|
|
bool : Type
|
|
Level : Type
|
|
|
|
|
|
Void : Ty
|
|
FlFun : Ty -> Ty -> Ty
|
|
Fun : bool -> Ty -> Ty -> Ty
|
|
|
|
Fixed : bool -> Level
|
|
Floating : bool -> Level
|
|
|
|
|
|
Abs : (bind Tm in Tm) -> Tm
|
|
FlAbs : (bind Tm in Tm) -> Tm
|
|
FlApp : Tm -> Tm -> Tm
|
|
App : Tm -> Tm -> Tm
|