Eta-reduce an expression

Stream: Is there code for X?

[Michael Rothgang]

Feel free to move this to the #lean4 stream; this is a metaprogramming question.

Is there code to eta-reduce a given Lean.Expr? I know about docs#Lean.Expr.beta (which does beta reduction), there's also zeta reduction, but no eta.

[Michael Rothgang]

I'd also be happy with an elaborator (is that the word) I can apply in the source to tell Lean "take this term, but eta-reduce it", as in

def f : Nat → Nat := id
-- Instead of this,
def g : Nat → Nat := fun n => f n
-- I'd like to do this (syntax invented)
def g' : Nat → Nat := eta% (fun n => f n)
-- to have `g'` be exactly `f`.

[Robin Arnez]

Doesn't docs#Lean.Expr.eta do eta-reduction?

[Michael Rothgang]

Huh, that's great! No idea why my loogling did not find that. Thank you!

[Michael Rothgang]

(Found that out now: I was searching for the string etaReduce, but eta would have found it. Lesson learned!)