编辑“︁Lean归纳类型”︁（章节）

== 简介 ==

归纳类型是通过一组构造子（constructors）递归定义的类型。每个构造子可以接受零个或多个参数，并返回该归纳类型的实例。在Lean中，归纳类型不仅用于表示数据结构（如列表、树），还能表示逻辑命题（如“真”、“假”或“存在”）。

归纳类型的定义遵循以下形式：
<syntaxhighlight lang="lean">
inductive MyType where
  | constructor₁ : Arg₁ → ... → Argₙ → MyType
  | constructor₂ : ... → MyType
  ...
</syntaxhighlight>

=== 基本示例：自然数 ===
自然数的归纳定义是经典的例子：
<syntaxhighlight lang="lean">
inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat
</syntaxhighlight>
这里：
* <code>zero</code> 是自然数0的构造子。
* <code>succ</code> 接受一个<code>Nat</code>类型的参数<code>n</code>，返回<code>n + 1</code>。

=== 递归与模式匹配 ===
归纳类型通常与递归函数和模式匹配结合使用。例如，计算自然数的加法：
<syntaxhighlight lang="lean">
def add : Nat → Nat → Nat
  | m, Nat.zero   => m
  | m, Nat.succ n => Nat.succ (add m n)
</syntaxhighlight>
输入 <code>add 2 3</code> 会逐步展开为 <code>Nat.succ (Nat.succ (Nat.succ 2))</code>，最终输出 <code>5</code>。