Logiweb(TM)

14.258 Deref-seqop used on undefined statement

Prev Up Next Page 729 of 800 Search internet


Origin: check. Landing-place: diagnose.

Deref-seqop used on undefined statement: R

The Deref sequent operator applied to a sequent << P ,, C ,, n >> yields << P ,, C ,, x >> where n is the name of a lemma and x is what the lemma says. Alternatively, n may be a theorem, axiom, theory, or whatever that has a statement definition. The 'Deref-seqop used on undefined statement' indicates that n did not denote any statement. The error may indicate an error in the proof or a bug in a tactic.

Prev Up Next Page 729 of 800 Search logiweb.eu

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