package dedukti

  1. Overview
  2. Docs
type term = private
  1. | Kind
  2. | Type of Basic.loc
  3. | DB of Basic.loc * Basic.ident * int
  4. | Const of Basic.loc * Basic.name
  5. | App of term * term * term list
  6. | Lam of Basic.loc * Basic.ident * term option * term
  7. | Pi of Basic.loc * Basic.ident * term * term
val pp_term : term Basic.printer
val get_loc : term -> Basic.loc
val mk_Kind : term
val mk_Type : Basic.loc -> term
val mk_DB : Basic.loc -> Basic.ident -> int -> term
val mk_Const : Basic.loc -> Basic.name -> term
val mk_Lam : Basic.loc -> Basic.ident -> term option -> term -> term
val mk_App : term -> term -> term list -> term
val mk_Pi : Basic.loc -> Basic.ident -> term -> term -> term
val mk_Arrow : Basic.loc -> term -> term -> term
val term_eq : term -> term -> bool
type untyped_context = (Basic.loc * Basic.ident) list
type typed_context = (Basic.loc * Basic.ident * term) list
val rename_vars_with_typed_context : typed_context -> term -> term