## 14.258 Deref-seqop used on undefined statement

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 yields 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.

Page 729 of 800 |
| Search logiweb.eu |

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