merge

abstract fun merge(substitution1: Substitution, substitution2: Substitution, occurCheckEnabled: Boolean): Substitution

Merges substitution1 and substitution2 into a single Substitution, as if their bindings had been collected while unifying two terms piecewise (e.g. argument by argument): equal-variable bindings from both sides are unified against each other and, optionally, checked for occurrence, rather than simply overwritten.

Return

the merged Substitution, or Substitution.failed if substitution1 and substitution2 disagree on some variable's binding (or either of them, or context, is already failed).


open fun merge(substitution1: Substitution, substitution2: Substitution): Substitution

Merges substitution1 and substitution2, with occurs-check enabled.