fstar - 这个引理减慢了 FStar/Emacs

Question

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

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

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

Answer 1

github.com/FStarLang/fstar-mode.el 上的文章将此问题称为 Emacs 错误。它似乎存在于 Emacs 26.3 中。Mx prettify-symbols-mode 解决它。