proof-general

1熱度

1回答

我正在使用ProqGeneral和Coq。當我進行C-C C返回時，Emacs會突出顯示Coq已處理的區域。這很好。但是，它在下一行插入'=>'，它會覆蓋輸入的前兩個字符。例如，目前我在看 Inductive Seq : Set := | MkSeq : Ants -> Form -> Seq. =>ductive Prf : Set := | Init : 我該如何擺脫那個箭頭？更

9熱度

1回答

Emacs下Coq/Proof General中關鍵字和運算符的Unicode字形

此問題與在Emacs中的Proof General內配置Coq模式有關。我試圖讓Emacs自動替換Coq中的關鍵字和符號以及相應的Unicode字形。我設法將fun定義爲希臘小寫lambdaλ，forall是通用量詞符號∀等。我沒有定義單詞符號的問題。問題是，當我嘗試將運算符=>,->, <->等等定義爲它們的Unicode符號⇒→↔時，它們不會被替換爲Coq中對應的Unicode字形。但是，

7熱度

2回答

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

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

4熱度

3回答

如何在emacs中禁用Verilog模式？

我試圖使用coq與ProofGeneral，但內置的Verilog模式陰影*.v文件類型識別。我可以以某種方式禁用它，讓ProofGeneral將它們重新映射到它的coq模式？

4熱度

1回答

如何在Isabelle/jEdit的假設中顯示括號？

當目標由伊莎貝爾在ProofGeneral顯示，假設被渲染爲具有身邊括號像這樣：在伊莎貝爾/ jEdit的，然而，這似乎已經改變到元蘊涵箭頭：雖然我理解前者是有點不標準，我覺得更容易閱讀。有沒有辦法修改Isabelle/jEdit的行爲來打印舊的ProofGeneral風格的目標？

0熱度

1回答

RegExp.exec如何填充其結果數組

我正在玩一些正則表達式，在查看我的一些匹配時，我開始好奇爲什麼exec函數會產生儘可能多的結果。我只是尋求操作的內部運作一個澄清一下，這樣我可以感覺更舒服爲什麼一個正則表達式返回ñ結果，而不是隻接受以爲然。 Ex。 var invalidValues = new RegExp( "\\bZIP or City & State$|" + "\\bCity & State or ZIP$|" +

1熱度

2回答

證明如果同時運行2個腳本，則一般抱怨腳本不完整

似乎PG不允許同時運行2個腳本。在嘗試這樣做的那一刻，Emacs會提示並要求撤消另一個文件。有時候，腳本不會重新運行。有沒有辦法在單個Emacs實例中真正運行2個（或更多）腳本？我認爲coqide gui沒有coq沒有這樣的問題。