Best font for proof assistants?

闲聊灌水
1

Proof assistant 会用到很多 unicode 字符，比如说 ℕ ⊎ ↦ ∨ ʳ ⇒ ⊤ ⟷

我目前是自己维护一个 list，用 dejavu sans mono 显示 list 里面的字符。几乎只有 dejavu sans mono 能显示得比较全，但有时不和自己的字体相称，这种情况大家是怎么搞的。

2

PLFA推荐了几个备选字体，现在首推用JuliaMono，之前首推的是mononoki。https://plfa.github.io/GettingStarted/#optional-using-the-juliamono-font-with-emacs

不过我个人感觉JuliaMono不如mononoki好看

我是偷懒直接按上述链接把默认字体设成mononoki了，你也可以用hook只在特定的mode启用这些字体。

1 个赞
4

推荐Iosevka term/fixed。
这三年一直在写Agda，一开始用mononoki（最好看），当notation多了起来后就少了不少symbol，JuliaMono个人观感没有Iosevka好看，而且字符数量比不上Iosevka。正常用agda-mode写unicode的话，输入法前两行的unicode几乎有适配到。

（抱歉上一个回复错人了orz）