dedukti

The Dedukti logical framework
IN THIS PACKAGE
Module Term
type term = private
| Kind
| Type of Basic.loc
| DB of Basic.loc * Basic.ident * int
| Const of Basic.loc * Basic.name
| App of term * term * term list
| Lam of Basic.loc * Basic.ident * term option * term
| 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