Coqプルーフスでの戦術の定義の位置付け

Question

他の作者のCoqプルーフを勉強する際に、私はしばしば "inv eq Heq"または "intro_b"と言うことができます。私はそのような戦術を理解したい。

現在のプロジェクトのどこかで定義されているCoq戦術またはTactic表記法は、どのようにして見つけることができますか？

第2に、その定義を見つける方法はありますか？

SearchAbout、Search、Locate and Printを使用しましたが、上記の質問に対する回答が見つかりませんでした。

Answer 1

ユーザー定義戦術（documentationに従って）のコードを印刷する

Print Ltac <tacticname>. 

を使用することができなければなりません。

---

、それが定義されている場所...私はあなたが、残念ながらのgrepを必要になるだろうと思い見つけるために、Locateは、それが思わ戦術名には使用できません。

Answer 2

前述したように、Print Ltac ...は、ユーザー定義の戦術のコードを出力します。

ユーザー定義の戦術を見つけるには（つまり、定義されている場所を知るため）、Locate Ltac ...を使用します。それはあなたに完全修飾名を与えます。次に対応するファイルを見つけるにはLocate Libraryを使います。