The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You can write "first [ has_evar L | has_evar R ]" or "has_evar L + has_evar R" or "tryif has_evar L then idtac else has_evar R".  You can make a tactic notation for any of these; I think `Tactic Notation tactic3(A) "or" tactic3(B)` should work.  Additionally, you may want to wrap the construction in "once"; I know "+" is multi-success (and am not sure about the others), so if you use "+" and don't wrap it in "once" then if you later fail, Coq will end up evaluating all the clauses if the "or" even if the first one succeeds.

On Sun, Dec 15, 2019, 11:17 Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Is there a way in Ltac to denote the logical disjunction of the conditionals fed to tryif?

I have

      tryif has_evar L
      then fail
      else
        tryif has_evar R
        then fail
        else some_tac.

I wish I could write it as:

      tryif (has_evar L or has_evar R)
      then fail
      else some_tac.

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/