Module Logtk__Term.Conv
type ctx
= Logtk.Type.Conv.ctx
val create : unit -> ctx
val of_simple_term : ctx -> Logtk.TypedSTerm.t -> t option
val of_simple_term_exn : ctx -> Logtk.TypedSTerm.t -> t
- raises Type.Conv.Error
on failure
val to_simple_term : ?allow_free_db:bool -> ?env:Logtk.TypedSTerm.t Logtk.Var.t Logtk.DBEnv.t -> ctx -> t -> Logtk.TypedSTerm.t
- raises Type.Conv.Error
on failure
val var_to_simple_var : ?prefix:string -> ctx -> var -> Logtk.TypedSTerm.t Logtk.Var.t