coq - Coq証明でタクティックの定義を見つける

Question

他の著者の Coq 証明を研究していると、"inv eq Heq" や "intro_b" などのタクティックに遭遇することがよくあります。そういう戦術を理解したい。

現在のプロジェクトのどこかで定義された Coq タクティックまたはタクティック記法であるかどうかを確認するにはどうすればよいですか?

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

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

Answer 1

あなたは使用できるはずです

Print Ltac <tacticname>.

ユーザー定義のタクティクスのコードを出力します (ドキュメンテーションに従って)。

---

定義されている場所を見つけるには...残念ながらgrepが必要になると思いますがLocate、戦術名では機能しないようです。

Answer 2

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

ユーザー定義の戦術を見つける (つまり、定義されている場所を知る) には、 を使用しますLocate Ltac ...。これにより、完全修飾名が提供されます。次に、 を使用Locate Libraryして対応するファイルを見つけます。