问这个引理减慢了FStar/Emacs的速度
EN

Stack Overflow用户

提问于 2020-05-18 15:48:50

回答 1查看 61关注 0票数 0

FStar需要大约2分钟来证明这个引理，更糟糕的是，Emacs在它存在的时候就会变得慢得令人难以忍受。其他的，显然更复杂的引理不会引起这个问题。

let lemma_1 (n: nat) (m: nat) : Lemma (n <= m || n > 0) = ()

是否有与此相关的Emacs/FStar选项？

回答已采纳

发布于 2020-05-19 17:56:47

github.com/FStarLang/fstar-mode.el上的文章提到这个问题是Emacs的一个bug。它似乎存在于Emacs 26.3中。M美化-符号-模式解决它。

票数 0

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/61873590

复制

相似问题

问这个引理减慢了FStar/Emacs的速度EN