14.291 Unknown unitac operator

Prev Up Next Page 762 of 800 Search internet

Origin: check. Landing-place: diagnose.

Unknown unitac operator in root of argumentation: t

During tactic expansion of the unification tactic x conclude y, the unification tactic does unitac expansion of x. During this unitac expansion, the unitac evaluator encountered an operator which was not a unitac tactic. The error message contains the entire term t which cannot be unitac expanded. The problematic operator is the principal operator of t.

The term t is given out of context and after macro expansion, so start out by locating the error.

Prev Up Next Page 762 of 800 Search logiweb.eu

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