# 元编程与宏

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

- 作者：David（道雾轩）
- 专栏：Lean 4 从入门到精通（https://daiw.org/manual/lean4.md）
- 最后更新：2026-10-01
- 原文：https://daiw.org/manual/lean4/metaprogramming
- 转载与引用：请注明出处并附原文链接（https://daiw.org/about/copyright）

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

## 三个层次

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

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

## notation：定义记号

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

#eval 3 ⊕ 4        -- 7
```

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

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

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

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

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

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

```lean
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：语法变换

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

#eval double 21     -- 42
```

拆解：

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

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

多条规则用 `macro_rules`：

```lean
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` | 宇宙层级 |

组合子：

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

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

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

## 自定义 tactic

```lean
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 组合封装成一个名字。

带参数的：

```lean
syntax "solve_with " term : tactic

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

## 卫生性

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

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

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

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

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

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

## elab：完全控制

```lean
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` 版本：

```lean
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
```

<Callout type="info">
  **元编程的 monad 层次**：

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

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

## 属性

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

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

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

@[myTag] def tagged : Nat := 42
```

## deriving handler

[前面](https://daiw.org/manual/lean4/inductive-types)用过 `deriving Repr`。自定义 deriving 也是元编程——写一个函数，输入类型的归纳结构，输出实例的定义。这是较高级的用法，Mathlib 里有多个例子可参考。

## 调试元编程

```lean
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。

**不该用**：

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

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

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

下一篇：[工程组织](https://daiw.org/manual/lean4/lake-projects)。