Module `Logtk__TypedSTerm.Subst`

type t = (term, term) Logtk.Var.Subst.t

val empty : t
val mem : t -> term Logtk.Var.t -> bool
val add : t -> term Logtk.Var.t -> term -> t: Add new binding to substitution Fails if the variable is bound already

val find : t -> term Logtk.Var.t -> term option

val find_exn : t -> term Logtk.Var.t -> term

raises Not_found: if the variable is not present

val rename_var : rename_binders:bool -> t -> term Logtk.Var.t -> t * term Logtk.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 Logtk.Interfaces.PRINT with type t := t

type t

val pp : t CCFormat.printer
val to_string : t -> string