val create : unit -> ctxval clear : ctx -> unitval enter_bvar : ctx -> VarMap.key -> int optionval exit_bvar : handle:int CCOpt.t -> ctx -> VarMap.key -> unitval find_bvar : ctx -> VarMap.key -> int optionval of_simple_term : ctx -> TypedSTerm.t -> t optionval var_of_simple_term : ctx -> TypedSTerm.t Var.t -> t HVar.tConvert a variable (and its type), and remember the binding.
val var_to_simple_var : ?prefix:string -> ctx -> t HVar.t -> TypedSTerm.t Var.texception Error of TypedSTerm.tval of_simple_term_exn : ctx -> TypedSTerm.t -> tInvalid_argument if conversion is impossible
val to_simple_term :
?env:TypedSTerm.t Var.t DBEnv.t ->
ctx ->
t ->
TypedSTerm.tconvert a type to a prolog term.
the current environment for De Bruijn indices