14.259 Deref-seqop produced non-meta term

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

Prev Up Next Page 730 of 800 Search logiweb.eu

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