Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC