lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

fix: reduce let-bodies correctly in `StructInst`

Open arthur-adjedj opened this issue 1 year ago • 1 comments

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.

arthur-adjedj avatar Jan 09 '24 14:01 arthur-adjedj

awaiting-review

arthur-adjedj avatar Mar 06 '24 22:03 arthur-adjedj