lean-0007: Declarations could use the kernel's _nested auxiliary type names
The kernel accepted user declarations named like the auxiliary types it generates for nested inductives, which let a bogus proof through. Reachable only through metaprogramming. nanoda and ind-models both rejected the bogus proof.
| Status | fixed |
|---|---|
| Fixed in | v4.33.0 |
| Subsystem | kernel |
| Guarantee broken | |
| Mechanism | |
| Symptom | — |
| Severity | unsoundness |
| Fools | |
| Discovery | |
| Features | |
| References |