7

ほとんどの IDE またはテキスト エディターでは、用語を右クリックすると、その用語が定義されているファイルに移動できます。CoqIDE にはそれがないようなので、私は を実行coqdoc myfile.v --htmlしてから、生成された HTML ドキュメントに移動しました。しかし、そのファイルでクリックできる用語は、Coq 標準ライブラリに関するものだけです。ssreflect で定義された用語 (たとえば) はクリックできません。

Coqファイルで、用語/識別子が定義されている場所(およびそのソースコード)をすばやく検索できる標準的な方法はありますか? CoqIDE または emacs + ProofGeneral (私は CoqIDE を使用していますが、emacs/ProofGeneral にこの機能があれば切り替えます)。

それとも、使用するすべての Coq プロジェクトと依存関係のドキュメントを生成する標準的な方法ですか?

4

2 に答える 2