Правильно ли ассоциируются тактики Coq или левые?

Question

Я изучал основы программного обеспечения и получил пример:

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

и был озадачен, что это значит.Например, мы получаем:

try [ (left; reflexivity); right ]

или

[try (left; reflexivity);] right

секунду или первую?

---

В частности, я пытался понять:

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

Answer 1

Хороший способ решить эти проблемы самостоятельно - использовать такие тактики, как idtac (всегда успешно) и fail (всегда неудачно) для устранения неоднозначности:

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

Так что, действительно, приложениеtry связывает крепче точки с запятой:

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