Stream: Coq users

Topic: Tactics: converting between semicolons and periods

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip Théo Winterhalter (Apr 30 2021 at 21:03):

Or 1-3: tactic.

Last updated: Jun 16 2024 at 02:41 UTC