Page 750 of 800
| 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 |