Stream: new members
Topic: tactics inside definitions
Bryan Gin-ge Chen (Oct 14 2018 at 22:47):
@Kenny Lau said:
You shouldn't use any tactics in a definition unless you know what you're doing, I think.
Why is this?
Kenny Lau (Oct 14 2018 at 22:48):
because it would be hxxx when you unfold the definition
Kevin Buzzard (Oct 14 2018 at 22:52):
The rule of thumb is: tactics generate weird proof terms. So sure use tactics when proving theorems (because the proof terms are forgotten) and you can even use tactics when defining complex things like
ring R for the bits which are proofs (e.g. proof of associativity) -- but the moment you use a tactic as part of a definition of some data it's not going to unfold well, making the definition hard to use in general.
Bryan Gin-ge Chen (Oct 14 2018 at 23:10):
Thanks, with the exception for "proof bits" of structures this makes much more sense. I just went through the code I've written and I've been more or less following this without knowing it.
Last updated: May 12 2021 at 03:23 UTC