504e099c5d
This PR replaces eager let-expression zeta-reduction in the sym-based mvcgen with on-demand unfolding that mirrors the production mvcgen's behavior. Previously, all let-expressions in the program head were immediately zeta-reduced. Now, let-expressions are hoisted to the top of the goal target, and the value is only inlined if it is duplicable (literals, fvars, consts, `OfNat.ofNat`). Complex values are introduced into the local context via `introsSimp`, preserving SymM's maximal sharing invariants, and unfolded on demand when the fvar later appears as the program head. --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
10 lines
255 B
Text
10 lines
255 B
Text
import Cases.AddSubCancel
|
|
import Cases.AddSubCancelDeep
|
|
import Cases.AddSubCancelSimp
|
|
import Cases.DiteSplit
|
|
import Cases.GetThrowSet
|
|
import Cases.LetBinding
|
|
import Cases.MatchIota
|
|
import Cases.MatchSplit
|
|
import Cases.PurePrecond
|
|
import Cases.ReaderState
|