Page 746 of 800
| Page 746 of 800 | Search internet |
Origin: check. Landing-place: diagnose.
Lemma L has no proof. Avoid referencing that lemma.
From the point of view of the verifier, a lemma is a symbol for which the home page of the symbol has both a statement definition and a proof definition. In contrast, axioms and theories are symbols which merely have a statement definition.
The 'Lemma L has no proof' message indicates that L is used as a lemma but does not have a proof. The error could be that a proof of L is missing or the error could be that e.g. an axiom was used as if it were a lemma.
Note that the verifier has no reservations about lemmas which have no proof. But the verifier protests if such a lemma is used as a lemma in the proof of some other lemma.
| Page 746 of 800 | Search logiweb.eu |