文本格式🔗

Verso 的完整格式说明见 Verso Markup。下面只列出本书最常用的功能。

插入行内 Lean 代码🔗

文档可以包含由 Lean 直接精译的代码，适合短小片段。代码仍应遵守 Lean 的命名、大小写等语法约定。

def helloCookbook := "Welcome!"

"Welcome!"#eval helloCookbook

可交互符号🔗

若希望正文中的 Lean 符号支持悬停信息和类型提示，请使用 {name} 与 {lean} role，而不是普通反引号。

{lean} `term`：精译一个完整的 Lean 表达式，例如 {lean}`1 + 2`。表达式中的每个 token 都会带有交互信息。
{name} `ConstName`：解析一个全局常量，例如 {name}`Nat`。悬停时显示其 docstring 和类型签名。

写法：

数字使用类型 {name}`Nat`。示例项可以写成 {lean}`[1, 2].map (· + 1)`。

效果：

渲染后，把鼠标悬停在 Nat 上会看到它的定义和 docstring。悬停在 [1, 2].map (· + 1) 的不同部分，则会看到列表、map 函数和 λ 抽象的类型。

文档字符串（docstring）🔗

Verso 可以通过 {docstring} role 把 Lean 定义的 docstring 直接嵌入文档。详细说明见这里。

{docstring Nat.add}

渲染结果如下：

def

Nat.add : Nat → Nat → Nat
Nat.add : Nat → Nat → Nat

Addition of natural numbers, typically used via the + operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

错误与警告🔗

若代码片段应当报错，可以像普通 Lean 文件一样在代码前使用 #guard_msgs。下面的例子来自在信息视图中显示内容配方。

def errorMessage' (msg : String) : CoreM Unit := do
  Lean.logError m!"Error: {msg}"

/-- error: Error: something went wrong -/
#guard_msgs in
#eval errorMessage' "something went wrong"

渲染结果如下：

def errorMessage' (msg : String) : CoreM Unit := do
  Lean.logError m!"Error: {msg}"

/-- error: Error: something went wrong -/
#guard_msgs in
#eval errorMessage' "something went wrong"

交叉引用🔗

通过 tag 可以链接其他章节：{ref "tag-name"}[链接文字]。

例如，源码 {ref "building-recipe"}[返回开头] 的效果是返回开头。

边注🔗

{margin}[边注文字] 会在页边显示补充内容，效果如下：边注适合补充不应打断正文的背景。

索引🔗

用 {index} role 把术语加入索引。它不会在正文中显示内容，只会在生成的索引中增加条目，例如 {index}[要索引的术语]。