编辑“︁Lean归纳定义”︁（章节）

== 基本概念 ==

在[[类型论]]中，归纳定义用于构造[[归纳类型]]（Inductive Types），这些类型通过一组构造子（constructors）来定义。每个构造子可以看作是该类型的"生成规则"。

归纳定义的一般形式如下：

<syntaxhighlight lang="lean">
inductive TypeName where
| constructor₁ : ArgumentTypes → TypeName
| constructor₂ : ArgumentTypes → TypeName
...
| constructorₙ : ArgumentTypes → TypeName
</syntaxhighlight>

=== 简单示例：自然数 ===

最经典的归纳类型是自然数的定义：

<syntaxhighlight lang="lean">
inductive Nat where
| zero : Nat
| succ (n : Nat) : Nat
</syntaxhighlight>

这个定义说明：
* '''zero''' 是一个自然数（基本情况）
* 如果 '''n''' 是一个自然数，那么 '''succ n'''（n的后继）也是一个自然数（归纳步骤）