14.280 Unknown tactic operator

Prev Up Next Page 751 of 800 Search internet

Origin: check. Landing-place: diagnose.

Unknown tactic operator in root of argumentation: t

During tactic expansion, the tactic evaluator encountered an operator which was not a tactic. The error message contains the entire term t which cannot be tactic 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 751 of 800 Search logiweb.eu

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