14.250 In seqcnt: Unknown seqop in root

Prev Up Next Page 721 of 800 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.

Prev Up Next Page 721 of 800 Search logiweb.eu

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