Stream: Coq users

Topic: is there a tactic for automating left/right.


view this post on Zulip walker (Feb 14 2023 at 15:52):

I have nested disjunctions, and I want something that automates only left/right choices.

I have things like this:

        right.
        left.
        left.
        by right.

in many places, and I want to avoid having to pick the path every single time ( Also I don't want to use auto because I prefer to have verbose proof control when it comes to applying lemmas and solving non trivial goals)

view this post on Zulip Gaëtan Gilbert (Feb 14 2023 at 15:55):

by repeat (left + right)?

view this post on Zulip walker (Feb 14 2023 at 15:57):

perfect, I didn't know about adding two tactics trick!

view this post on Zulip Alexander Gryzlov (Feb 14 2023 at 21:25):

do !constructor maybe too?


Last updated: May 18 2024 at 08:40 UTC