## Stream: general

### Topic: beta reduction tactic

#### Kenny Lau (Aug 12 2020 at 16:39):

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

#### Kevin Buzzard (Aug 12 2020 at 17:02):

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 (Aug 12 2020 at 17:04):

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

Last updated: May 12 2021 at 05:19 UTC