SymM-level head-redex reducer used throughout VCGen.

def Lean.Elab.Tactic.Do.Internal.VCGen.reduceHead? (e : Expr) : Meta.Sym.SymM (Option Expr)

Repeatedly reduces head redexes in e, cycling through the following reductions until no further progress is made:

1. Beta: (fun x₁ ... xₘ => b) a₁ ... aₙ → b[a₁/x₁, aₘ/xₘ] aₘ₊₁ ... aₙ
2. Iota: MyType.casesOn (MyType.ctor args) alts → altᵢ args (matcher/recursor applied to a constructor, at reducible transparency)
3. Proj-reduction: ⟨a, b, c⟩.1 → a (kernel .proj nodes)
4. Projection delta: Struct.field x → x.5 (unfolds projection functions, progress only if followed by proj-reduction)

Returns none when no reduction was possible. Maintains maximal sharing via shareCommonInc.

Equations

• Lean.Elab.Tactic.Do.Internal.VCGen.reduceHead? e = Lean.Meta.withReducible (Lean.Elab.Tactic.Do.Internal.VCGen.reduceHead?.go✝ none e.getAppFn e.getAppRevArgs)

def Lean.Elab.Tactic.Do.Internal.VCGen.reduceHead (e : Expr) : Meta.Sym.SymM Expr

Equations

• Lean.Elab.Tactic.Do.Internal.VCGen.reduceHead e = do let __do_lift ← Lean.Elab.Tactic.Do.Internal.VCGen.reduceHead? e pure (__do_lift.getD e)