预览：

% <![CDATA[
\DeclareMathOperator{Set}{Set}
\DeclareMathOperator{where}{where}
\DeclareMathOperator{proof}{proof}
\DeclareMathOperator{data}{data}
\DeclareMathOperator{rev}{rev}
\DeclareMathOperator{ff}{ff}
\DeclareMathOperator{lemma}{lemma}
\DeclareMathOperator{intro}{intro}
\DeclareMathOperator{id}{id}
\DeclareMathOperator{refl}{refl}
\DeclareMathOperator{params}{params}
\DeclareMathOperator{Vec}{Vec}
\DeclareMathOperator{rewrite}{rewrite}
\DeclareMathOperator{with}{with}
\DeclareMathOperator{lhs}{lhs}
\DeclareMathOperator{rhs}{rhs}
\DeclareMathOperator{xs}{xs}

\begin{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
\end{align*} %]]>

渲染测试：

$$ \DeclareMathOperator{Set}{Set} \DeclareMathOperator{where}{where} \DeclareMathOperator{proof}{proof} \DeclareMathOperator{data}{data} \DeclareMathOperator{rev}{rev} \DeclareMathOperator{ff}{ff} \DeclareMathOperator{lemma}{lemma} \DeclareMathOperator{intro}{intro} \DeclareMathOperator{id}{id} \DeclareMathOperator{refl}{refl} \DeclareMathOperator{params}{params} \DeclareMathOperator{Vec}{Vec} \DeclareMathOperator{rewrite}{rewrite} \DeclareMathOperator{with}{with} \DeclareMathOperator{lhs}{lhs} \DeclareMathOperator{rhs}{rhs} \DeclareMathOperator{xs}{xs} \begin{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 \end{align*} $$

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

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

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

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

你的姿势可能不对…… * 被 markdown 转换成 _ 了……

$$\DeclareMathOperator{Set}{Set} \DeclareMathOperator{where}{where} \DeclareMathOperator{proof}{proof} \DeclareMathOperator{data}{data} \DeclareMathOperator{rev}{rev} \DeclareMathOperator{ff}{ff} \DeclareMathOperator{lemma}{lemma} \DeclareMathOperator{intro}{intro} \DeclareMathOperator{id}{id} \DeclareMathOperator{refl}{refl} \DeclareMathOperator{params}{params} \DeclareMathOperator{Vec}{Vec} \DeclareMathOperator{rewrite}{rewrite} \DeclareMathOperator{with}{with} \DeclareMathOperator{lhs}{lhs} \DeclareMathOperator{rhs}{rhs} \DeclareMathOperator{xs}{xs}$$

\begin{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 \end{align}

那应该是markdown太垃圾了。我们换个渲染器吧。

或者改下源码重新编译个markdown吧。