def Lean.Meta.Sym.etaReduce (e : Expr) : Expr

If e is of the form (fun x₁ ... xₙ => f x₁ ... xₙ) and f does not contain x₁, ..., xₙ, then returns f. Otherwise, returns e.

Returns the original expression when not reducible to enable pointer equality checks.

Equations

• Lean.Meta.Sym.etaReduce e = Lean.Meta.Sym.etaReduce.go✝ e e 0

def Lean.Meta.Sym.isEtaReducible (e : Expr) : Bool

Returns true if e can be eta-reduced. Uses pointer equality for efficiency.

Equations

• Lean.Meta.Sym.isEtaReducible e = !Lean.Meta.Sym.isSameExpr e (Lean.Meta.Sym.etaReduce e)

def Lean.Meta.Sym.etaReduceAll (e : Expr) : MetaM Expr

Applies etaReduce to all subexpressions. Returns e unchanged if no subexpression is eta-reducible.

Equations

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