coqide

2熱度

1回答

我使用frama-C WP並希望調試我的ACSL註釋（瞭解爲什麼證明者說我「不知道」）。我有一些綠色或橙色的結果。我打開why3 IDE並查看生成的腳本。然後我從列表中選擇一個理論/目標，並能夠啓動Alt-Ergo或Coq IDE。我想在Coq IDE中使用生成的代碼。我看到一些公理定理，然後WP 然後，例如： intros a a_1 i_3 i_2 i_1 i t_2 t_1 t t_8 t

2熱度

2回答

Vim插件無法識別現有的Perl支持

我一直在Linux機器上使用CoqIDE plugin for Vim來編輯Coq文件。現在，我想在Windows 8安裝它，但，當我嘗試源插件，我得到 Your vim doesn't support Perl. Install it before using CoqIDE mode. 這很奇怪，因爲我:version清楚地看到包括+perl/dyn。這與我需要的+perl不同嗎？我聽說你

1熱度

2回答

CoqIDE 8.5默認字體

對不起，這個小問題--- CoqIDE在Coq 8.5中的默認字體是什麼？嘗試Coq 8.6 w/nix-shell -p coq_8_6 --run coqide改變了我的舊CoqIDE字體（和鍵綁定）;我想讓他們回來，但不記得字體名稱。確切的版本（不知道這是否重要）是8.5pl1。可悲的是，重啓，甚至nix-env --rollback沒有恢復的設置（我的8.5安裝瓦特/ nix和nix-sh

0熱度

1回答

CoqIDE和JAVA

我想檢索一個文件的編譯結果。 v來自coqide或coqc用java處理，而我有一個自動機的處理，我想在java中構建這個自動機的圖形界面。感謝您的回覆。

7熱度

2回答

Coq/Proof General中的Agda-like編程？

與Agda不同，Coq傾向於將證據與功能分開。 Coq提供的策略非常適合寫作證明，但我想知道是否有方法來複制某些Agda模式功能。具體來說，我想：阿格達的?或Haskell的_，在那裏我可以省略的部分功能的一些等價，而我寫它，（希望）有勒柯克告訴我鍵入我需要把有抄送Cr的阿格達模式（物化），等效在那裏你填寫一個?塊具有的功能，它將使新?塊所需的參數當我在做什麼一個函數中有一個match，C

6熱度

1回答

在當前環境中未找到參考「X」

我正在使用CoqIDE完成軟件基礎本手冊中關於Coq的練習。我可以成功編譯Basics.v，在我的目錄中生成Basics.vo和Basics.glob。當我嘗試運行Induction.v時，它可以工作。當我嘗試編譯它時，它會抱怨大量缺失的引用，如evenb和negb_involutive。如果我將Basics.v內容複製到Induction.v中，它會進行編譯，但顯然這不是要走的路。這不是問題C