Module Substs.FO

module FO: SPECIALIZED  with type term = FOTerm.t

type term

type t = Substs.subst

val find_exn : t ->
       Substs.var Scoped.t -> term Scoped.t

val get_var : t ->
       Substs.var Scoped.t -> term Scoped.t option

val deref : t ->
       term Scoped.t -> term Scoped.t

val apply : t ->
       renaming:Substs.Renaming.t ->
       term Scoped.t -> term

Apply the substitution to the given term/type.

renaming : used to desambiguate free variables from distinct scopes

val apply_no_renaming : t ->
       term Scoped.t -> term

Same as Substs.SPECIALIZED.apply, but performs no renaming of free variables. Caution, can entail collisions between scopes!

val bind : t ->
       Substs.var Scoped.t ->
       term Scoped.t -> t

Add v -> t to the substitution. Both terms have a context.
Raises InconsistentBinding if v is already bound in the same context, to another term.