tactic vs option

Stream: metaprogramming / tactics

[Damiano Testa]

Dear All,

Sometimes, I have the choice of making a meta def with values in tactic _ or in option _. I have an instinctive preference for option.

Are there reasons for preferring tactic instead? Or to prefer it systematically?

Thanks!

[Eric Wieser]

If you use tactic you can set an error message

[Eric Wieser]

Usually your hand is forced by needing to call an API that is itself a tactic _

[Damiano Testa]

Eric Wieser said:

If you use tactic you can set an error message

Thanks, Eric! Yes, I am slowly understanding how to use errors more extensively and it helps in making changes to the tactic.

Eric Wieser said:

Usually your hand is forced by needing to call an API that is itself a tactic _

Yes, it is not often that I have the choice. Maybe this is the reason why, when I can, then I feel that I should take advantage of it! :smile:

[Yakov Pechersky]

But as soon as you make something tactic, that means anything that uses it needs the be at least as powerful as tactic itself.

[Damiano Testa]

While we are in this discussion, is there any speed optimization that is achieved by using or avoiding tactic? My instinct says that it might be slower to go via tactic, but maybe I am wrong and maybe it is largely irrelevant. :shrug:

[Eric Wieser]

I would assume it's largely irrelevant