| Search internet |
Origin: check. Landing-place: diagnose.
In seqcnt: Unknown seqop in root of t
This is the same as the previous error message except that the error if found not by the verifier but by the seqcnt function. The seqcnt function counts the number of sequent operators in a sequent term. The seqcnt function may be useful during development of efficient tactics.
| Search logiweb.eu |