Are Coq tacticals right associative or left associ

问题:

I was going through software foundations and got the example:

repeat (try (left; reflexivity); right).

and was confused what this meant. For example do we get:

try [ (left; reflexivity); right ]

or

[try (left; reflexivity);] right

second or first?

---

in particular I was trying to understand:

Theorem In10 : In 10 [1;2;3;4;5;6;7;8;9;10].
Proof.
  repeat (try (left; reflexivity); right).
Qed.

回答1:

A good way of solving those problems on your own is to use tactics like idtac (always succeeds) and fail (always fails) to disambiguate:

try (idtac; idtac); fail.     (* FAILS *)
try ((idtac; idtac); fail).   (* SUCCEEDS *)
(try (idtac; idtac)); fail.   (* FAILS *)

So indeed, the application of try binds tighter than the semicolon:

try (idtac; idtac); fail.   is the same as   (try (idtac; idtac)); fail.