Module Make.S

module Cof = Kado.Syntax.Endo
type t =
  1. | Var of int
  2. | Global of Symbol.t
  3. | Let of t * Ident.t * t
  4. | Ann of t * tp
  5. | Zero
  6. | Suc of t
  7. | NatElim of t * t * t * t
  8. | Base
  9. | Loop of t
  10. | CircleElim of t * t * t * t
  11. | Lam of Ident.t * t
  12. | Ap of t * t
  13. | Pair of t * t
  14. | Fst of t
  15. | Snd of t
  16. | Struct of fields
  17. | Proj of t * Ident.t * int
  18. | Coe of t * t * t * t
  19. | HCom of t * t * t * t * t
  20. | Com of t * t * t * t * t
  21. | SubIn of t
  22. | SubOut of t
  23. | Dim0
  24. | Dim1
  25. | Cof of (t, t) Cof.t
  26. | ForallCof of t
  27. | CofSplit of (t * t) list
  28. | Prf
  29. | ElIn of t
  30. | ElOut of t
  31. | Box of t * t * t * t * t
  32. | Cap of t * t * t * t * t
  33. | VIn of t * t * t * t
  34. | VProj of t * t * t * t * t
  35. | CodeExt of int * t * [ `Global of t ] * t
  36. | CodePi of t * t
  37. | CodeSg of t * t
  38. | CodeSignature of kan_tele
  39. | CodeNat
  40. | CodeUniv
  41. | CodeV of t * t * t * t
  42. | CodeCircle
  43. | ESub of sub * t
and tp =
  1. | Univ
  2. | El of t
  3. | TpVar of int
  4. | TpDim
  5. | TpCof
  6. | TpPrf of t
  7. | TpCofSplit of (t * tp) list
  8. | Sub of tp * t * t
  9. | Pi of tp * Ident.t * tp
  10. | Sg of tp * Ident.t * tp
  11. | Signature of tele
  12. | Nat
  13. | Circle
  14. | TpESub of sub * tp
and tele =
  1. | ElTele of kan_tele
  2. | Cell of Ident.t * tp * tele
  3. | Empty
and kan_tele =
  1. | KCell of Ident.t * t * kan_tele
  2. | KEmpty
and fields =
  1. | Fields of (Ident.t * t) list
  2. | Unpack of Ident.t list * t
  3. | MCoe of Ident.t * kan_tele * t * t * fields
  4. | MCom of kan_tele * t * t * t * fields
and sub =
  1. | SbI
  2. | SbC of sub * sub
  3. | Sb1
  4. | SbE of sub * t
  5. | SbP
module CofBuilder : sig ... end
val tm_abort : t
val tp_abort : tp
val tele_lbls : tele -> Ident.t list
val kan_tele_lbls : kan_tele -> Ident.t list
val rename_tele : (Ident.t -> Ident.t option) -> tele -> tele
val rename_kan_tele : (Ident.t -> Ident.t option) -> kan_tele -> kan_tele
val append_tele : tele -> tele -> tele
val append_kan_tele : kan_tele -> kan_tele -> kan_tele
val pp_sequent : lbl:string option -> (Ident.t * tp) list -> tp Basis.Pp.printer
val pp_partial_sequent : [< `BdrySat | `BdryUnsat ] -> (Ident.t * tp) list -> (t * tp) Basis.Pp.printer
val dump : t Basis.Pp.printer
val dump_tele : tele Basis.Pp.printer
val dump_kan_tele : kan_tele Basis.Pp.printer
val dump_tp : tp Basis.Pp.printer