Stream: Coq users

Topic: Solving all remaining subgoals in a proof

view this post on Zulip Alessandro Bruni (Nov 21 2023 at 10:31):

Hi! I have a proof with two different subgoals that are solved by exactly the same proof script, which is long and I don't want to compact. I know of the all: tactic, but is there something similar that allows me to solve two similar subgoals with a sub script?

view this post on Zulip Karl Palmskog (Nov 21 2023 at 10:39):

is there a reason not to use number-based goal selectors? For example:

tac. 1-3,5,8-9,11: done.

view this post on Zulip Alessandro Bruni (Nov 21 2023 at 10:42):

I'm not familiar with that, can you point me to the documentation?

view this post on Zulip Julin Shaji (Nov 21 2023 at 10:43):

This may be it: https://coq.inria.fr/refman/proof-engine/ltac.html#grammar-token-range_selector

view this post on Zulip Alessandro Bruni (Nov 21 2023 at 10:56):

Thanks both!

Last updated: Oct 13 2024 at 01:02 UTC