看这个帖子有感——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}

预览： % <![CDATA[ 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}

egin{align*} data F : Bbb{N} rightarrow Set where ff : (n : Bbb{N}) rightarrow F n

proof _0 : {n : Bbb{N}} rightarrow F n rightarrow F n rightarrow F n proof _0 (ff n) (ff {.}n) = ff n nd{align*} %]]>