coqでlists.vをコンパイルするには？

私は補助証拠COQを使用しています。私の最初の質問は、Induction.vファイルについてです。Require Import basicsの代わりにRequire Export Basicsを使用するのはなぜですか？また、基本名をMybasics.vに変更した場合でも、Export basics.vを作成すると、なぜ機能しますか？coqでlists.vをコンパイルするには？

Require Export Basics.は何をしますか？それはインポートまたはエクスポートですか？

それはライブラリの誘導を見つけることが

ができないと言い、私はinduction.vをコンパイルした後lists.vを実行しようとしましたが、それは動作しません。

どうすれば修正できますか？

出典

2017-10-28 elle believe

あなたはソフトウェア基盤に取り組んでいますか？ COQPATHにフォルダを追加する必要があります。証拠の一般はそれを処理したので、私はあなたがcoqideを使用していると思いますか？

残りのご質問は、coq ref manual：https://coq.inria.fr/refman/toc.htmlを参照して解決してください。

出典

2017-10-29 01:45:18 HuStmpHrrr

私はそれが答えに行かなければならないことを私には分かりません。あなたがcoqを学んでいる間にあなたが遭遇するすべての質問を尋ねようとすれば、それは手ごわいものです。ドキュメントは常にあなたの最初の友達です。どのように物事がどのようにレベルまで働くかを理解することを学ぶ必要があります。 – HuStmpHrrr

Require ImportとRequire Exportの違いはここで見つけることができます：コンパイルに関する詳細な情報を提供https://coq.inria.fr/refman/vernacular.html#hevea_command115

（例えばあなたは、コマンドラインまたはコードエディタを使用していたかどうか、コックのバージョン、教科書のバージョンなど）可能性がありあなたの問題を解決するのに役立ちます。

出典

2017-11-01 04:12:44

coqでlists.vをコンパイルするには？

答えて

関連する問題