tactics inside definitions

Stream: new members

[Bryan Gin-ge Chen]

@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]

because it would be hxxx when you unfold the definition

[Kevin Buzzard]

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]

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.