Правильно ли ассоциируются тактики 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.