Implements (syntactic) higher-order pre-unification for term pairs based on projection and imitation.
Summary
Functions
Implements depth-bounded higher-order pre-unification to solve a unification problem consisting of a single term pair or a list of term pairs. Returns a lazy stream of unification solutions.
Functions
@spec unify([term_pair()] | term_pair(), non_neg_integer()) :: Enumerable.t(ShotUn.UnifSolution.t())
Implements depth-bounded higher-order pre-unification to solve a unification problem consisting of a single term pair or a list of term pairs. Returns a lazy stream of unification solutions.