Page 744 of 800
| Page 744 of 800 | Search internet |
Origin: check. Landing-place: diagnose.
Lemma P occurs on a page with a non-empty diagnose. Avoid referencing that lemma.
When a proof references a lemma on another page, the verifier checks two things: First, that the other page has been proof checked. Second, that the outcome of verification was positive.
The verifier checks that the outcome of verification was positive by looking at the diagnose hook of the rack of the other page. The diagnose is empty or true when it has value 
. The error indicates that the diagnose was not and thus the referenced page was in error and the referenced lemma may be false.
Note that the verifier has no reservations about incorrect pages in general. Even if a page has a non-empty diagnose, it may contain useful definitions. But the verifier protests the moment one uses a lemma from an incorrect page.
| Page 744 of 800 | Search logiweb.eu |