SyntaxData.Make
module Symbol : Basis.Symbol.S
type t =
| Var of int
| Global of Symbol.t
| Let of t * Ident.t * t
| Ann of t * tp
| Zero
| Suc of t
| NatElim of t * t * t * t
| Base
| Loop of t
| CircleElim of t * t * t * t
| Lam of Ident.t * t
| Ap of t * t
| Pair of t * t
| Fst of t
| Snd of t
| Struct of fields
| Proj of t * Ident.t * int
| Coe of t * t * t * t
| HCom of t * t * t * t * t
| Com of t * t * t * t * t
| SubIn of t
| SubOut of t
| Dim0
| Dim1
| Cof of (t, t) Cof.t
| ForallCof of t
| CofSplit of (t * t) list
| Prf
| ElIn of t
| ElOut of t
| Box of t * t * t * t * t
| Cap of t * t * t * t * t
| VIn of t * t * t * t
| VProj of t * t * t * t * t
| CodeExt of int * t * [ `Global of t ] * t
| CodePi of t * t
| CodeSg of t * t
| CodeSignature of kan_tele
| CodeNat
| CodeUniv
| CodeV of t * t * t * t
| CodeCircle
| ESub of sub * t
Explicit substition
*)and fields =
| Fields of (Ident.t * t) list
| Unpack of Ident.t list * t
Unpack a Struct
into its list of fields.
| MCoe of Ident.t * kan_tele * t * t * fields
Coercion along a line in a telescope. The kan_tele has a free variable for a dimension variable.
*)| MCom of kan_tele * t * t * t * fields
Composition in a telescope, provided a list of systems.
*)The language of substitions from Abel, Coquand, and Pagano.
module CofBuilder : sig ... end