etaExpandAll — Mathlib

Lean4
/-- Eta expand every sub-expression in the given expression.

As a side-effect, beta reduces any pre-existing instances of eta expanded terms. -/
partial def etaExpandAll (e : Expr) : MetaM Expr := do
  let betaOrApp (f : Expr) (args : Array Expr) : Expr := if f.etaExpanded?.isSome then f.beta args else mkAppN f args
  let expand (e : Expr) : MetaM Expr := do
    if e.isLambda then
      return e
    else
      forallTelescopeReducing (← inferType e) fun xs _ => do
          mkLambdaFVars xs (betaOrApp e xs)
  transform e (pre := fun node => do
      if node.isApp then
        let f ← etaExpandAll node.getAppFn
        let args ← node.getAppArgs.mapM etaExpandAll
        .done <$> expand (betaOrApp f args)
      else
        pure .continue)
      (post := (.done <$> expand ·))
Похожие утверждения