Module LogtkSubsts.FO

module FO: SPECIALIZED  with type term = LogtkFOTerm.t

type term 
type t = LogtkSubsts.subst 
val mem : t ->
term -> LogtkSubsts.scope -> bool
Variable is bound?
val apply : t ->
renaming:LogtkSubsts.Renaming.t ->
term ->
LogtkSubsts.scope -> term
Apply the substitution to the given term/type.
renaming : used to desambiguate free variables from distinct scopes
val apply_no_renaming : t ->
term ->
LogtkSubsts.scope -> term
Same as LogtkSubsts.SPECIALIZED.apply, but performs no renaming of free variables. Caution, can entail collisions between scopes!
val bind : t ->
term ->
LogtkSubsts.scope ->
term ->
LogtkSubsts.scope -> t
Add v -> t to the substitution. Both terms have a context.
Raises Invalid_argument if v is already bound in the same context, to another term.