Page 720 of 800
| 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.
| Page 720 of 800 | Search logiweb.eu |