flattening a lambda

Stream: new members

[Alex Meiburg]

What's the easiest way to turn (fun x => p x) into just p? Is this definitionally equivalent or what? simp does it but I try to avoid it, and simp? doesn't tell me how

(also tips on how to look this up in the future are welcome)

[Yongyi Chen]

I think it's beta_reduce.

[Alex Meiburg]

Hmm, seems close but no cigar: "This means that whenever there is an applied lambda expression such as (fun x => f x) y then the argument is substituted into the lambda expression yielding an expression such as f y."

[Alex Meiburg]

Oh, found it. :) It's eta_reduce. Thanks for the tip in the right direction!

[Alex J. Best]

I would do simp only or dsimp only to do this sort of reduction normally. Nothing wrong with eta_reduce per se but it requires you having to remember which Greek letter is which