Coq リファレンス マニュアル (8.5p1) を読んでいます。
戦術のローカル適用
次の形式を使用して、さまざまな目標にさまざまな戦術を適用できます。
[ > expr1 | ::: | 式]
exprii = 0の場合、式は vi に評価されます。...; n そしてすべてが戦術でなければなりません。= 1 の場合、vi は i 番目のゴールに適用されます。...; n. フォーカスされたゴールの数が正確に n でない場合、失敗します。
idtacそこで、次のように、それぞれに2 つの些細な戦術を適用しようとする 2 つの目標を使用して、簡単なテストを行いました。
Goal forall P Q: Prop, P \/ Q -> Q \/ P.
intros. destruct H. [ > idtac | idtac ].
ただし、予想される戦術は 1 つだけであるというエラーが表示されました。
エラー: ゴール数が正しくありません (予想される 1 つの戦術)。
よくわかりません。誰かが私が間違ったことを説明できますか?正しい使用法は何ですか?