Companion

Same as allOf, but taking the two Terms as a Pair (pair.first = lhs, pair.second = rhs).

Recursively decomposes lhs and rhs into a (possibly empty) sequence of Equations, none of which is a Comparison between structurally-matching compound terms: lists, tuples and structs sharing the same functor/arity are unfolded and paired element-wise (recursing into each pair), rather than being classified as a single Comparison the way of would. This is what AbstractUnificator uses to expand a pair of Terms into the equations it then simplifies to compute an MGU.

Same as from, for an Iterable of Pairs.

Applies allOf to every Pair in pairs, concatenating the resulting fully-decomposed Equations.

Same as from, for a vararg of Pairs.

Same as of, but taking the two Terms as a Pair (pair.first = lhs, pair.second = rhs).

Classifies lhs and rhs into the appropriate Equation subtype: Identity if they are trivially equal (per equalityChecker, or structurally for variables), LeftAssignment/RightAssignment if exactly one side is a Var, Contradiction if they can be told apart at this level (different constants, or structs with different functor/arity), or Comparison if they need further decomposition (e.g. two structs with the same functor/arity, whose arguments are not inspected by this shallow classification — use allOf to recursively decompose down to non-decomposable equations).