|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 with by instantiating to and to . But the unification tactic cannot unify with .
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.
|Page 750 of 800||Search logiweb.eu|