Joshua Grosso (Apr 30 2021 at 20:08): Joshua Grosso (Apr 30 2021 at 20:08):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.)
Li-yao (Apr 30 2021 at 20:34):As an intermediate solution there are goal selectors. all: mytactic. or 1: mytactic. or 1,2: mytactic.
Théo Winterhalter (Apr 30 2021 at 21:03):Or 1-3: tactic.
Last updated: Sep 23 2023 at 14:01 UTC