CodeUnit.Domain
module S : sig ... end
module CofVar : sig ... end
module Dim : sig ... end
module Cof : sig ... end
type dim = Dim.t
type cof_var = CofVar.t
type cof = Cof.t
type !'a stable_code = [
|
`Circle
|
`Ext of int * 'a * [ `Global of 'a ] * 'a
|
`Nat
|
`Pi of 'a * 'a
|
`Sg of 'a * 'a
|
`Signature of kan_tele
|
`Univ
]
and kan_tele_clo = S.kan_tele clo
and con =
| Lam of Ident.t * tm_clo
| BindSym of DimProbe.t * con
| LetSym of dim * DimProbe.t * con
| Cut of {
}
| Zero
| Suc of con
| Base
| Loop of dim
| Pair of con * con
| Struct of fields
| SubIn of con
| ElIn of con
| Dim0
| Dim1
| DimProbe of DimProbe.t
| Cof of (con, con) Kado.Syntax.endo
| Prf
| FHCom of [ `Circle | `Nat ] * dim * dim * cof * con
| StableCode of con stable_code
| UnstableCode of con unstable_code
| Box of dim * dim * cof * con * con
| VIn of dim * con * con * con
| Split of (cof * tm_clo) list
module CofBuilder : sig ... end
val fst : con
val snd : con
val el_out : con
val tm_abort : con
val tp_abort : tp
val empty_env : env
val pp_dim : dim Basis.Pp.printer
val pp_clo : tm_clo Basis.Pp.printer
val pp_cof : cof Basis.Pp.printer
val pp_tp : tp Basis.Pp.printer
val pp_con : con Basis.Pp.printer
val pp_cut : cut Basis.Pp.printer
val pp_hd : hd Basis.Pp.printer
val pp_frame : frm Basis.Pp.printer
val pp_spine : frm list Basis.Pp.printer
val pp_tele : tele Basis.Pp.printer
val pp_kan_tele : kan_tele Basis.Pp.printer