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没有这样的问题。