Is {...} a tactic?

Stream: general

[Jason Rute]

I'm starting to understand the interactive tactics and how they work and are implemented. Is the focus notation {...} which focuses on the first goal a tactic? It seems similar to tactic.focus1 (tac >> done) where tac is the inner tactic.

[Mario Carneiro]

It is focus

[Mario Carneiro]

{ tac } is the same as focus {tac}, and you can read the interactive tactic here

[Jason Rute]

No. focus doesn't error if you don't complete the goal. I think it is solve1, partly because that is the same behavior and partly because if you don't finish a {...} block, the error is solve1 tactic failed, focused goal has not been solved. :upside_down:

[Jason Rute]

(I think the lesson is that error messages can tell you a lot. I should look there more often.)