transform `fun a => f a` back to `f`?

Stream: Is there code for X?

[Scott Morrison]

Surely there is a function Expr → Expr that "cancels" function application and lambda abstraction at the top level of the expression, and does nothing else. But what would it be called?

[Jireh Loreaux]

That's eta reduction for function types, so presumably it has eta in the name? Just a guess.

[Kyle Miller]

There's docs4#Lean.Expr.eta for going from the function to f and docs4#Lean.Meta.etaExpand for something like its inverse.