14.249 Unknown seqop in root

Prev Up Next Page 720 of 800 Search internet

Origin: check. Landing-place: diagnose.

Unknown seqop in root of t

The verifier expects the outcome of tactic expansion to be a sequent term built up from the thirteen sequent operators of the Logiweb sequent calculus. Those operators are: Init, Ponens, Probans, Verify, Curry, Uncurry, Dereference, at, infer, endorse, id est, all, and cut. The 'Unknown seqop in root' message indicates that the term t does not have one of the thirteen operators as principal operator. The error may indicate an error in the proof or a bug in a tactic. Also see the next error message.

Prev Up Next Page 720 of 800 Search logiweb.eu

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