fix: reduce let-bodies correctly in `StructInst` (#3152) 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.
This is the repository for Lean 4.
See Setting Up Lean.
Please read our Contribution Guidelines first.
See Building Lean (documentation source: doc/make/index.md).