lean-0013: Exported stubs of partial definitions were not marked unsafe
The stubs exported for partial definitions were not marked unsafe. Caught while exporting an exploit during the FRO's bug hunt; not a soundness bug on its own.
| Status | fixed |
|---|---|
| Fixed in | v4.33.0 |
| Subsystem | elaborator |
| Guarantee broken | — |
| Mechanism | — |
| Symptom | — |
| Severity | hardening |
| Fools | — |
| Discovery | |
| Features | |
| References |