Lean-zh / fp-lean-zh

Lean 函数式编程
https://www.leanprover.cn/fp-lean-zh/
Other
25 stars 7 forks source link

[Formatting] 中文粗体未能正常渲染 #28

Closed skylee03 closed 2 months ago

skylee03 commented 2 months ago

image

当加粗部分以标点符号(如右括号)结尾时,右 ** 的右侧必须是有空格、换行或者其他标点。

PLFA-zh 的内容在 GitHub 直接显示时也常有同样的问题,但是其网页版可以正常渲染。

https://github.com/Agda-zh/PLFA-zh/issues/1 的示例为例。

修改前:

现在我们定义了自然数及其运算,下一步是学习如何证明它们满足的性质。
如其名称所示,**归纳数据类型(inductive datatype)**是通过**归纳(induction)**
来证明的。

现在我们定义了自然数及其运算,下一步是学习如何证明它们满足的性质。 如其名称所示,归纳数据类型(inductive datatype)是通过归纳(induction) 来证明的。

修改后:

现在我们定义了自然数及其运算,下一步是学习如何证明它们满足的性质。
如其名称所示,**归纳数据类型(inductive datatype)** 是通过**归纳(induction)**
来证明的。

现在我们定义了自然数及其运算,下一步是学习如何证明它们满足的性质。 如其名称所示,归纳数据类型(inductive datatype) 是通过归纳(induction) 来证明的。

skylee03 commented 2 months ago

此外,在 Markdown 文件内换行会引入多余的空格。

image

image

OlingCat commented 2 months ago

此外,在 Markdown 文件内换行会引入多余的空格。

image

image

断行的空格我写了个预处理脚本来去掉。不正确的粗体显示我再想想办法。

OlingCat commented 2 months ago

通过在渲染端添加了 JS 脚本移除了多余的空格,并修复了加粗问题。具体见 https://github.com/Lean-zh/fp-lean-zh/commit/afa8de51a604d436cb6ec286150b17a290a8f068