Henrik Böving
|
85645958f9
|
fix: overeager specialisation reuse in codegen (#10429)
This PR fixes and overeager reuse of specialisation in the code
generator.
The issue was originally discovered in
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Miscompilation.20.28incorrect.20code.29.20in.20new.20compiler/near/540037917
and occurs because the specialisation cache didnt't take the name of
alternatives in pattern matches
into account.
|
2025-09-17 17:35:40 +00:00 |
|