beta reduction tactic

Stream: general

[Kenny Lau]

Should we have a beta reduction tactic, or is dsimp only equivalent to one?

[Kevin Buzzard]

I think a beta tactic which could be run on goals and hypotheses would be great. It would help to teach mathematicians what beta reduction is. I don't even know myself -- I had to look it up before I answered, but it's certainly not uncommon that I see students with (\lam x, f x) (37) in their goal or context (I just tell them dsimp right now). We have classical.some_spec but still have a choose tactic. Is there a reason for not having a beta tactic?

[Reid Barton]

Seems like a good idea to me even if the definition is just a one-liner calling dsimp with the correct arguments