您可能熟悉Lean或某些函数式编程语言中的模式匹配，因此这里有一个使用此机制的解决方案：
open natdefinition pred : ? �� ?
| zero := zero
| (succ n) := n</code>
另一种方法是使用像这样的recursor：
def pred (n : ?) : ? :=
nat.recon n 0 (�� p , p)</code>
这里，
0
如果参数为零，我们返回的是
(�� p _, p)
是一个匿名函数，它有两个参数：前身（
p
）的
n
和递归调用的结果
pred p
。匿名函数忽略第二个参数并返回前一个参数。