code wiki / proof
topic: proof
13 modules sharing the proof name family (derived from the tree's prefix discipline).
| module | description | lines | funcs |
|---|---|---|---|
| nx_proof.nx | Checks for grammatical and stylistic errors in prose without relying on external dictionaries. | 299 | 12 |
| nx_proof_emit.nx | two-column proof emitter. | 138 | 4 |
| nx_proof_infinitude_primes.nx | Euclid's proof that there are | 98 | 1 |
| nx_proof_infinitude_primes_test.nx | exercise Euclid IX.20. | 32 | 1 |
| nx_proof_log.nx | inference history tracking. | 121 | 5 |
| nx_proof_log_test.nx | proof history tracking smoke. | 91 | 1 |
| nx_proof_methods.nx | comprehensive sealed enum of proof methods | 97 | 4 |
| nx_proof_sqrt2_irrational.nx | HONEST kernel-checked derivation of | 135 | 1 |
| nx_proof_sqrt2_irrational_test.nx | exercise the honest sqrt(2) proof. | 46 | 1 |
| nx_proof_sqrt2_v2.nx | sqrt(2) is irrational, with REAL semantic | 110 | 1 |
| nx_proof_sqrt2_v2_test.nx | exercise the sqrt(2) proof using the | 33 | 1 |
| nx_proof_sqrt2_v3.nx | sqrt(2) is irrational, RESULT IS A CLOSED | 78 | 1 |
| nx_proof_sqrt2_v3_test.nx | exercise the CLOSED v3 proof. | 29 | 1 |