module Subst:sig
..end
type
t
typescope =
int
type
renaming
val empty : t
Empty subst
val bind : t ->
TopDown.S.T.t ->
scope ->
TopDown.S.T.t -> scope -> t
Bind a variable,scope to a term,scope
val deref : t ->
TopDown.S.T.t ->
scope -> TopDown.S.T.t * scope
While the term is a variable bound in subst, follow its binding. Returns the final term and scope
val create_renaming : unit -> renaming
val reset_renaming : renaming -> unit
val rename : renaming:renaming ->
TopDown.S.T.t -> scope -> TopDown.S.T.t
Rename the given variable into a variable that is unique
within variables known to the given renaming
val eval : t ->
renaming:renaming ->
TopDown.S.T.t -> scope -> TopDown.S.T.t
Apply the substitution to the term. Free variables are renamed
using renaming
val eval_lit : t ->
renaming:renaming ->
TopDown.S.Lit.t -> scope -> TopDown.S.Lit.t
val eval_lits : t ->
renaming:renaming ->
TopDown.S.Lit.t list -> scope -> TopDown.S.Lit.t list
val eval_clause : t ->
renaming:renaming ->
TopDown.S.C.t -> scope -> TopDown.S.C.t