编辑“︁Lean递归函数”︁（章节）

== 基本概念 ==

在Lean中，递归函数必须满足'''终止性'''（Termination）条件，即所有递归调用必须作用于"更小"的参数，以确保计算最终会停止。这与数学归纳法的原理紧密相关。

递归函数的定义通常包含两个部分：
* '''基例'''（Base Case）：处理最简单的情况，无需递归
* '''递归情况'''（Recursive Case）：将问题分解为更小的子问题

=== 简单示例：阶乘函数 ===

以下是用Lean定义的阶乘函数：

<syntaxhighlight lang="lean">
def factorial : Nat → Nat
| 0     => 1  -- 基例：0! = 1
| n + 1 => (n + 1) * factorial n  -- 递归情况：(n+1)! = (n+1) * n!
</syntaxhighlight>

'''输入输出示例'''：
* `#eval factorial 5` → 120
* `#eval factorial 0` → 1