参照 "X"は現在の環境で見つかりませんでした

Question

私はCoqについてのソフトウェア基礎の練習を完了するためにCoqIDEを使用しています。私は正常にBasics.vをコンパイルすることができます。その結果、Basics.voとBasics.globが私のディレクトリにあります。 Induction.vを実行しようとすると、動作します。私がコンパイルしようとすると、それはevenbとnegb_involutiveのような数多くの欠落した参照に文句を言う。 Basics.vの内容をInduction.vにコピーすると、コンパイルされますが、明らかにこれはやり方ではありません。

コンパイルBasics.v：私はすでにそれらの事を行っているよう

これは、質問Coq error: The reference evenb was not found in the current environmentの複製ではありません。 Basics.voがディレクトリにあるかどうか確認してください。今すぐInduction.vをコンパイルしてください。この最後のステップは失敗します。

Answer 1

私はこのエラーを自分で経験しました。ソフトウェア基盤ファイルと同じディレクトリからCoqIDEを開き、そこでコンパイルしてください。 Linuxの場合は、端末を開いてそのディレクトリに移動し、そこでcoqideと入力します。私は他のシステムでこれをどうやって行うのかはよく分かりません。 Mac OSでは、アイコンを使ってアプリを開くだけで失敗することに気がつきました。