## 14.259 Deref-seqop produced non-meta term

Page 730 of 800 |
| Search internet |

Origin: check. Landing-place: diagnose.

**Deref-seqop applied to R produced non-meta term: R prime**

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 produced non-meta term' indicates that the statement definition of n is illformed.

Page 730 of 800 |
| Search logiweb.eu |

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