問題タブ [coqide]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
95 問題
0
投票する
1
に答える
1508
参照
coq - 同じライブラリ内のモジュールをエクスポートする際の CoqIDE エラー
CoqIDE を実行して教科書シリーズ「ソフトウェアの基礎」を読んでいます。現在、「論理的な基礎」を読んでいます。2章(誘導編)を始めたばかりですが、ラインを走らせようとすると
エラーステートメントが表示されます
The file ...\LF\Basics.vo contains library
Basics and not library LF.Basics
ファイルが置かれているディレクトリの名前を変更して、バッファを再コンパイルしようとしましたが、これらのアクションはどちらも役に立ちませんでした。この問題を解決するにはどうすればよいですか?