lean4
lean4 copied to clipboard
fix: reduce let-bodies correctly in `StructInst`
Closes #3146
Reduction doesn't trigger correctly on the bodies of let-expressions in StructInst, leading some meta-variables to linger in the terms of some fields. Because of this, default fields may try multiple times (and fail) to be generated, leading to an unexpected error.
The solution implemented here is to modify the values of the introduced variables in the local context so as to reduce them correctly.
awaiting-review