package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
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