sig
type t
type scope = int
type renaming
val empty : TopDown.S.Subst.t
val bind :
TopDown.S.Subst.t ->
TopDown.S.T.t ->
TopDown.S.Subst.scope ->
TopDown.S.T.t -> TopDown.S.Subst.scope -> TopDown.S.Subst.t
val deref :
TopDown.S.Subst.t ->
TopDown.S.T.t ->
TopDown.S.Subst.scope -> TopDown.S.T.t * TopDown.S.Subst.scope
val create_renaming : unit -> TopDown.S.Subst.renaming
val reset_renaming : TopDown.S.Subst.renaming -> unit
val rename :
renaming:TopDown.S.Subst.renaming ->
TopDown.S.T.t -> TopDown.S.Subst.scope -> TopDown.S.T.t
val eval :
TopDown.S.Subst.t ->
renaming:TopDown.S.Subst.renaming ->
TopDown.S.T.t -> TopDown.S.Subst.scope -> TopDown.S.T.t
val eval_lit :
TopDown.S.Subst.t ->
renaming:TopDown.S.Subst.renaming ->
TopDown.S.Lit.t -> TopDown.S.Subst.scope -> TopDown.S.Lit.t
val eval_lits :
TopDown.S.Subst.t ->
renaming:TopDown.S.Subst.renaming ->
TopDown.S.Lit.t list -> TopDown.S.Subst.scope -> TopDown.S.Lit.t list
val eval_clause :
TopDown.S.Subst.t ->
renaming:TopDown.S.Subst.renaming ->
TopDown.S.C.t -> TopDown.S.Subst.scope -> TopDown.S.C.t
end