14.279 Unable to unify t with u

Prev Up Next Page 750 of 800 Search internet

Origin: check. Landing-place: diagnose.

Unable to unify t with u

The unification tactic tried to instantiate t and u to make them equal (i.e. tried to unify t and u). As an example, the tactic can unify 2 * 3 + #x with #y + 4 * 5 by instantiating #x to 4 * 5 and #y to 2 * 3. But the unification tactic cannot unify 2 * 3 + #x with #y - 4 * 5.

Locating the error may be problematic because t and u are given out of context. The message indicates which proof line of which proof is in error. Often, that is enough to locate the error.

Prev Up Next Page 750 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05