I find it super-unwieldy to convert between periods and semicolons in tactics, especially in the presence of bullets—e.g. if I realize I can use the same proof procedure for multiple subgoals, which themselves have several subgoals. Is there a generalized solution to this (other than using
[... | ...] & co. everywhere)?
(Personally, I prefer periods so that I can use bullets, step through proofs, etc., so it makes me sad to have to abandon those benefits so often.)
As an intermediate solution there are goal selectors.
all: mytactic. or
1: mytactic. or
Last updated: Jan 27 2023 at 01:03 UTC