元编程与宏

notation/macro/elab 三个层次、语法范畴与卫生性，以及写自定义 tactic 的基本骨架。

Lean 用 Lean 自己写——编译器前端、几乎所有 tactic、do 记法都是用 Lean 的元编程能力实现的。这意味着扩展语言不需要学第二套语言。

三个层次

层次	命令	能力	复杂度
记号	`notation` / `infixl`	定义中缀/前缀记号	低
宏	`macro` / `macro_rules`	语法到语法的变换	中
繁饰器	`elab`	直接构造 `Expr`，可访问类型信息	高

能用低层次就别用高层次——notation 能表达的不要写 macro。

notation：定义记号

notation:65 a " ⊕ " b => Nat.add a b

#eval 3 ⊕ 4        -- 7

:65 是优先级——决定它与其他记号的结合紧密程度。数字越大越紧。参考值：

优先级	例子
65	`+` `-`
70	`*` `/`
75	`^`
50	`=` `<` `≤`
35	`∧`
30	`∨`
25	`→` `↔`

结合性用专门的命令更方便：

infixl:65 " ⊕ " => Nat.add      -- 左结合
infixr:67 " ⊗ " => Nat.mul      -- 右结合
prefix:max "‖" => Nat.succ
postfix:max "!" => Nat.factorial

记号里的空格是有意义的：" ⊕ " 两边的空格决定了解析与显示的间距。漏掉会导致 a⊕b 无法解析或显示难看。

带作用域的记号（避免污染全局）：

namespace MyLib
scoped notation:65 a " ⊕ " b => Nat.add a b
end MyLib

-- 只有 open MyLib 之后才可用
open MyLib in
#eval 3 ⊕ 4

Mathlib 大量使用 scoped——不同数学分支的记号可能冲突（如 ⟪x, y⟫ 在内积与配对里都用）。

macro：语法变换

macro "double " x:term : term => `($x * 2)

#eval double 21     -- 42

拆解：

macro "double " x:term : term => `($x * 2)
      ^^^^^^^^^ ^^^^^^   ^^^^    ^^^^^^^^^
      字面量    参数     产出的  展开结果
                及其     语法    (反引号是 quotation)
                范畴     范畴

反引号 `(...) 是 quotation——它构造语法树而不是求值。$x 是 antiquotation，把变量插进去。

多条规则用 macro_rules：

syntax "myif " term " then " term " else " term : term

macro_rules
  | `(myif $c then $t else $e) => `(if $c then $t else $e)

#eval myif true then 1 else 2      -- 1

syntax 先声明语法形状，macro_rules 再给出展开——比 macro 灵活（可以有多条规则、可以后续追加）。

语法范畴

范畴	含义
`term`	表达式
`tactic`	tactic
`command`	顶层命令
`ident`	标识符
`num`	数字字面量
`str`	字符串字面量
`level`	宇宙层级

组合子：

syntax "mylist" "[" term,* "]" : term      -- 逗号分隔，任意个
syntax "myopt" (term)? : term              -- 可选
syntax "myrep" term+ : term                -- 一个或多个

macro_rules
  | `(mylist [ $elems,* ]) => `([$elems,*])

#eval (mylist [1, 2, 3] : List Nat)   -- [1, 2, 3]

自定义 tactic

syntax "my_trivial" : tactic

macro_rules
  | `(tactic| my_trivial) => `(tactic| first | rfl | simp | omega)

example : 2 + 2 = 4 := by my_trivial
example (n : Nat) : n + 0 = n := by my_trivial

这是最实用的元编程场景——把你反复写的 tactic 组合封装成一个名字。

带参数的：

syntax "solve_with " term : tactic

macro_rules
  | `(tactic| solve_with $h) => `(tactic| first | exact $h | simp [$h:term] | omega)

卫生性

macro "swap_test" : term => `(let tmp := 1; tmp)

def tmp := 999
#eval swap_test        -- 1，不是 999

Lean 的宏是卫生的（hygienic）：宏内部引入的名字不会与使用处的名字冲突。

这解决了 C 宏的经典问题——不必担心你的临时变量名撞上用户的变量名。

需要故意捕获用户作用域的名字时，要显式处理：

macro "with_x " body:term : term => `(fun x => $body)
-- body 里的 x 不会绑到这个 x（卫生性），需要用 antiquotation 传入

elab：完全控制

open Lean Elab Term Meta in
elab "my_check " t:term : term => do
  let e ← elabTerm t none
  let ty ← inferType e
  logInfo m!"type: {ty}"
  return e

#check my_check (2 + 2)

elab 让你直接操作 Expr（Lean 的内部项表示），可以：

查询类型（inferType）
求解元变量
访问局部上下文
生成任意项

代价是复杂度陡增——需要理解 MetaM、TermElabM、TacticM 这些 monad 层次。

自定义 tactic 的 elab 版本：

open Lean Elab Tactic in
elab "print_goal" : tactic => do
  let goal ← getMainGoal
  logInfo m!"{← goal.getType}"

example (n : Nat) : n = n := by
  print_goal      -- 打印 n = n
  rfl

元编程的 monad 层次：

CoreM     基础：环境、名字生成
  ↓
MetaM     + 元变量、类型推断、defeq 检查
  ↓
TermElabM + 语法繁饰
  ↓
TacticM   + 目标管理

外层能调用内层（用 liftM 或自动提升）。写 tactic 用 TacticM，写 term 繁饰器用 TermElabM。

属性

@[simp] theorem foo : ... := ...
@[ext] theorem bar : ... := ...
@[simp, norm_cast] theorem baz : ... := ...

属性把定理注册进各种自动化的规则集。自定义属性也是元编程：

open Lean in
initialize myAttr : TagAttribute ←
  registerTagAttribute `myTag "my custom tag"

@[myTag] def tagged : Nat := 42

deriving handler

前面用过 deriving Repr。自定义 deriving 也是元编程——写一个函数，输入类型的归纳结构，输出实例的定义。这是较高级的用法，Mathlib 里有多个例子可参考。

调试元编程

set_option pp.all true in
#check 1 + 1              -- 显示完全展开的项

set_option pp.explicit true in
#check @Nat.add           -- 显示所有隐式参数

set_option trace.Elab true in
example : True := trivial  -- 打印繁饰过程

选项	显示
`pp.all`	一切细节
`pp.explicit`	隐式参数
`pp.universes`	宇宙层级
`pp.notation false`	关闭记号，看原始形式
`trace.Elab`	繁饰过程
`trace.Meta.synthInstance`	实例解析过程

set_option pp.all true in #check e 是理解「Lean 到底看到了什么」的得力手段。当记号让你困惑时，把它关掉。

什么时候该用元编程

该用：

反复出现的 tactic 组合 → 自定义 tactic。
领域特定的记号 → notation。
样板代码生成 → macro 或 deriving handler。

不该用：

能用普通函数表达的 → 写函数。
只用一两次的 → 直接写。
为了「显得高级」→ 元编程让代码更难读，要有明确收益。

元编程的错误信息很差。 宏展开出错时，报错位置常常指向展开后的代码而不是你写的地方。

写宏时先手工写出展开后的目标代码，确认它能工作，再包装成宏。这样出问题时能立刻定位是宏的问题还是逻辑的问题。

下一篇：工程组织。

本页目录