let-to-have for SymM

Sym.letToHave converts nondependent let declarations of a term into have declarations (i.e., sets the nondep flag of .letE nodes). The result is definitionally equal to the input, has exactly the same shape, and preserves maximal sharing: only the nodes on the path from the root to each converted let are rebuilt.

A let x := v; b is nondependent if b typechecks with x opaque. As in Meta.letToHave, this is decided with the withTrackingZetaDelta technique: the body is checked with x declared as a zeta-expandable declaration, and x is nondependent iff no check needed to unfold it. Unlike Meta.letToHave, the traversal:

• keeps bodies in bound-variable form — no instantiate/abstract round-trip per binder, which makes the traversal near-linear on nested binders with open bodies (Meta.letToHave is quadratic there);
• discharges checking obligations only on subterms that can reach a candidate let: subterms without loose bound variables, and subterms whose loose bound variables all refer to "clean" binders, are skipped in O(1);
• discharges each obligation via pointer equality (the usual case in the maximally shared world), falling back to the tracked Meta.isDefEq.

instantiate is used in exactly two places: to put a binder's type (and value, for a let) into free-variable form before adding the scratch declaration to the local context, and to put terms into free-variable form before inferType/isDefEq calls.

Caching follows the two-tier discipline of Sym.liftLets: results and inferred types for terms with loose bound variables are cached per binder scope (the scoped caches are saved and reset when entering a binder body, and restored on exit — entries computed at an outer binder offset must be invisible inside), while results for closed terms are context-free and cached for the whole run; closed-term types go through the session Sym.inferType cache.

Metavariables are opaque for the analysis (the whole run is under withNewMCtxDepth, so pre-existing metavariables are rigid for isDefEq and can never be assigned by an obligation), but a dependent let whose subtree contains one is conservatively kept: a future assignment could depend on the let variable's value. Metavariables outside a let's subtree do not inhibit its conversion.

def Lean.Meta.Sym.letToHave (e : Expr) : SymM Expr

Converts the nondependent let declarations of e into have declarations. The result is definitionally equal to e, has the same shape (only nondep flags change), and is maximally shared. If nothing is converted, the result is pointer-equal to e (check with isSameExpr).

Assumptions: e is maximally shared, has no loose bound variables, and is type correct. Metavariables are treated as opaque values.

Equations

• One or more equations did not get rendered due to their size.