Lean 4(元)编程 Cookbook

元数据与标签🔗

每个标题下面都可以定义元数据:

%%%
tag := "my-tag"
number := false
htmlSplit := .never
%%%

以后可以通过 tag 引用这一节。

怎样取得 tag 对应的链接? 在网页中点击标题并跳转到该节,浏览器 URL 中会出现这个 tag。

  • 说明 1htmlSplit := .never 是可选项,只在不想把本节拆成多个页面时使用。本书的 Verso 配置为 htmlDepth := 3。在达到第三层深度之前,# 标题会生成子页面,而不是留在当前页面。如果确定不应分页,就在元数据中加入这一行。

  • 说明 2:本书不是按固定顺序阅读的线性教材,而是可以直接跳到任意条目的参考手册,因此用 number := false 关闭编号。