package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
type ctx
val create : unit -> ctx
val copy : ctx -> ctx
val clear : ctx -> unit
val enter_bvar : ctx -> VarMap.key -> int option
val exit_bvar : handle:int CCOpt.t -> ctx -> VarMap.key -> unit
val find_bvar : ctx -> VarMap.key -> int option
val get_maxvar : ctx -> int
val incr_maxvar : ctx -> unit
val set_maxvar : ctx -> int -> unit
val of_simple_term : ctx -> TypedSTerm.t -> t option

convert a simple typed term into a type. The term is assumed to be closed.

  • returns

    an error message if the term is not a type

  • parameter ctx

    context used to map Var to HVar

val var_of_simple_term : ctx -> TypedSTerm.t Var.t -> t HVar.t

Convert a variable (and its type), and remember the binding.

val fresh_ty_var : ctx -> t HVar.t

Fresh type variable

val var_to_simple_var : ?prefix:string -> ctx -> t HVar.t -> TypedSTerm.t Var.t
exception Error of TypedSTerm.t
val of_simple_term_exn : ctx -> TypedSTerm.t -> t
val to_simple_term : ?env:TypedSTerm.t Var.t DBEnv.t -> ctx -> t -> TypedSTerm.t

convert a type to a prolog term.

  • parameter env

    the current environment for De Bruijn indices