coqide

2熱

2答えて

Coqide 8.5 w/nixがインストールされました。残念ながら、テキストはすべてのパネルでblakcです。どのような種類の構文も強調表示されていません（そうでなければ、8.5も私がインストールした8.4よりも大幅に改善されているようです）。私はまた、次を得る： (coqide:17272): GtkSourceView-WARNING **: Unknown parent scheme 'c

1熱

1答えて

Coqをインストールするには

WindowsとMacの両方でhttps://coq.inria.fr/のダウンロードリンクを使用してCoqをインストールしています。しかし、端末またはコマンドプロンプトでcoqcまたはcoqtopを試すと、コマンドが見つからないというエラーメッセージが表示されます。 Coq IDEでCoqをほぼ完璧に動かすことができますが、バッファをコンパイルすると、特にSoftware Foundations

6熱

1答えて

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

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

2熱

1答えて

なぜcoqでスクリプトを生成したのかを証明する方法は？

私はframa-C WPを使用し、ACSLアノテーションをデバッグしたいと思います。緑色またはオレンジ色の結果があります。私はなぜIDE3を開き、生成されたスクリプトを参照してください。その後、リストから理論/目標を選択し、Alt-ErgoまたはCoq IDEを起動することができます。私はCoq IDEで生成されたコードで遊びたいです。私は、例えば、その後、その後、定理WP いくつかの公理を見て

0熱

2答えて

CoqのXMLプロトコル文書の「editId」とは何ですか？

Coq's XML Protocol document (for the Add operation)には、<int>${editId}</int>と表示されています。ここでeditIDは何ですか？私はサイドバイトモードでcoqtopと対話できなかったため、これを尋ねました。例としてcoq-8.6.1/theories/FSets/FSetCompat.vを使用して、私は <call val="

3熱

1答えて

なぜcoqideで_CoqProjectを使って `make 'するのがコマンドラインで` coqc`と違うのですか？

私は2つの短いファイルを持っている：cc_testが Lemma cc: 4 = 4. Proof. auto. Qed. によって与えられ、libtestは私が実行 Require Import cc_test. Check cc. で与えられるディレクトリ内coqc -R . ClosureLib -top ClosureLib cc_test "/ホーム/バリー/ SVN /コック/ Cl

1熱

1答えて

Coqideキーバインディングのバグ

私は最近、私はつまり、CoqIDEを使用しながら、生じたいくつかの奇妙な状況に持ってきた...奇妙な問題のビットを持ってる（？）：私はできませんウィンドウ/スーパーキーを押さずに文字 "v"を入力してください。複数のウィンドウが開いている場合、バックスペースを押すと前のタブにフォーカスが移動しますが、そのオブジェクトを削除することはできません。 CTRL +バックスペースはチャンクを削除するた

2熱

1答えて

LinuxのCoqIDE設定

私は、Ubuntu 17.04にCoq 8.6を新しくインストールしました。 makeを使ってプロジェクトをコンパイルしようとすると、最初のエラーメッセージが出るまでうまく動作します。そして、このように、私は、エラーを見つけて修正するためにCoqIDEを使用しようと、私は新しいエラーメッセージが出ます：「ファイルfoo.voは、ライブラリTop.fooとライブラリではないのfooが含まれている」

1熱

2答えて

CoqIDE 8.5の既定のフォント

この簡単な質問は申し訳ありません--- Coq 8.5のCoqIDEの既定のフォントは何ですか？ Coq 8.6 w/nix-shell -p coq_8_6 --run coqideを試してみましたが、私の古いCoqIDEフォント（とキーバインディング）を変更しました。私はそれらを元に戻したいが、フォント名は覚えていない。正確なバージョン（これが問題なのかどうかわからない）は8.5pl1です。悲

7熱

2答えて

Coq/Proof GeneralのAgdaのようなプログラミングですか？

Agdaとは異なり、Coqは証明と機能を分離する傾向があります。 Coqが提供する戦術は、校正を書くのに最適ですが、Agdaモードの機能を再現する方法があるかどうかは疑問です。具体的には、私がしたい： Agdaの?やHaskellの_の一部と同等に、私はそれを書いている間、機能の一部を省略し、（たぶん）コックは私伝える持つことができる場所タイプ私はあなたが機能して?ブロックを埋めるAgdaモード