lean-0011: Missing metavariable and free-variable checks in inductive.cpp
inductive.cpp was missing check_no_metavar_no_fvar checks. 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 | kernel |
| Guarantee broken | — |
| Mechanism | |
| Symptom | — |
| Severity | hardening |
| Fools | — |
| Discovery | |
| Features | — |
| References |