logtk

Core types and algorithms for logic
IN THIS PACKAGE
Module Logtk . TypedSTerm . Subst
type t = ( term, term ) Var.Subst.t
val empty : t
val mem : t -> term Var.t -> bool
val add : t -> term Var.t -> term -> t

Add new binding to substitution Fails if the variable is bound already

val find : t -> term Var.t -> term option
val find_exn : t -> term Var.t -> term
  • raises Not_found

    if the variable is not present

val rename_var : rename_binders:bool -> t -> term Var.t -> t * term Var.t
val merge : t -> t -> t
val eval : ?rename_binders:bool -> t -> term -> term
val eval_nonrec : t -> term -> term

Evaluate under substitution, but consider the substitution as not idempotent

include Interfaces.PRINT with type t := t
val to_string : t -> string