Zulip Chat Archive

Stream: new members

Topic: tactics inside definitions


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Oct 14 2018 at 22:48):

because it would be hxxx when you unfold the definition

view this post on Zulip 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.

view this post on Zulip 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