package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Type.ConvSource

Sourcetype ctx
Sourceval create : unit -> ctx
Sourceval copy : ctx -> ctx
Sourceval clear : ctx -> unit
Sourceval enter_bvar : ctx -> VarMap.key -> int option
Sourceval exit_bvar : handle:int CCOpt.t -> ctx -> VarMap.key -> unit
Sourceval find_bvar : ctx -> VarMap.key -> int option
Sourceval 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

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

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

Sourceval fresh_ty_var : ctx -> t HVar.t

Fresh type variable

Sourceval var_to_simple_var : ?prefix:string -> ctx -> t HVar.t -> TypedSTerm.t Var.t
Sourceexception Error of TypedSTerm.t
Sourceval of_simple_term_exn : ctx -> TypedSTerm.t -> t
Sourceval 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