logtk

Core types and algorithms for logic
IN THIS PACKAGE
Module Logtk . Term . Conv
type ctx = Type.Conv.ctx
val create : unit -> ctx
val of_simple_term : ctx -> TypedSTerm.t -> t option
val of_simple_term_exn : ctx -> TypedSTerm.t -> t
  • raises Type.Conv.Error

    on failure

val to_simple_term : ?allow_free_db:bool -> ?env:TypedSTerm.t Var.t DBEnv.t -> ctx -> t -> TypedSTerm.t
val var_to_simple_var : ?prefix:string -> ctx -> var -> TypedSTerm.t Var.t