Page 229 of 800
| Page 229 of 800 | Search internet |
The claim definition of the check page reads:
That statement macro expands into a claim definition of the page construct of the check page.
The 
construct is defined on the base page:
Hence, the verifier of the check page is a conjunction of two verifiers: the test1 verifier from the base page which verifies test cases and a new one called proofcheck which happens to check proofs.
The two verifiers are executed left to right. If test1 finds an error in a test case then proofcheck is not invoked.
A page which does not define a verifier of its own and which references the check page as first reference is verified by both test1 and proofcheck. A page with does not define a verifier of its own and which references the base page as first reference is merely verified by test1. Hence, it is entirely up to the author of a page what should be verified.
If you want to test your pages e.g. for type correctness w.r.t. some typing system you like, then write a type checker and include it in your conjunction of verifiers.
| Page 229 of 800 | Search logiweb.eu |