希望改进为： 只用编译一次，中间过程全部走内存，可选辅助文件是否输出 原生支持unicode 字体选择，原生提供字体回退和自由分区 支持更多图片类型 提高图文混排功能 提高编译器的「智能程度」，减少行间公式环境的数量 其实相当于，基于目前的软硬件水平重新设计和制造。知乎有人估计过，以 google 水平的薪资，大概需要10人*年的工作量。

看这个帖子有感——PyTorch 有哪些坑/bug？——不知道类型系统能不能帮助。

那应该是markdown太垃圾了。我们换个渲染器吧。 或者改下源码重新编译个markdown吧。

你的姿势可能不对…… * 被 markdown 转换成 _ 了…… DeclareMathOperator{Set}{Set} eclareMathOperator{where}{where} eclareMathOperator{proof}{proof} eclareMathOperator{data}{data} eclareMathOperator{rev}{rev} eclareMathOperator{ff}{ff} eclareMathOperator{lemma}{lemma} eclareMathOperator{intro}{intro} eclareMathOperator{id}{id} eclareMathOperator{refl}{refl} eclareMathOperator{params}{params} eclareMathOperator{Vec}{Vec} eclareMathOperator{rewrite}{rewrite} eclareMathOperator{with}{with} eclareMathOperator{lhs}{lhs} eclareMathOperator{rhs}{rhs} eclareMathOperator{xs}{xs} begin{align} amp; data F : Bbb{N} rightarrow Set where amp; ff : (n : Bbb{N}) rightarrow F n

amp; proof _0 : {n : Bbb{N}} rightarrow F n rightarrow F n rightarrow F n amp; proof _0 (ff n) (ff {.}n) = ff n nd{align}

谢谢虎哥 虎哥 人间的真男人 虎哥 我的偶像

虎哥，这个社区的槽点让我想虎哥化了。

在知乎，类似的 LaTeX 代码渲染正常。 只是这篇博客还没转载到知乎，就暂时参考的老博客。

LaTeX 代码出处： http://ice1000.org/2017/11/09/ProofInAgda5/ 的第一个代码块。

目前的状况：垃圾的一比，我空个行就识别错误了。

渲染测试：
eclareMathOperator{Set}{Set} eclareMathOperator{where}{where} eclareMathOperator{proof}{proof} eclareMathOperator{data}{data} eclareMathOperator{rev}{rev} eclareMathOperator{ff}{ff} eclareMathOperator{lemma}{lemma} eclareMathOperator{intro}{intro} eclareMathOperator{id}{id} eclareMathOperator{refl}{refl} eclareMathOperator{params}{params} eclareMathOperator{Vec}{Vec} eclareMathOperator{rewrite}{rewrite} eclareMathOperator{with}{with} eclareMathOperator{lhs}{lhs} eclareMathOperator{rhs}{rhs} eclareMathOperator{xs}{xs} begin{align} amp; data F : Bbb{N} rightarrow Set where amp; ff : (n : Bbb{N}) rightarrow F n

amp; proof _0 : {n : Bbb{N}} rightarrow F n rightarrow F n rightarrow F n amp; proof _0 (ff n) (ff {.}n) = ff n nd{align}