定義精益自然數的前驅函數（pred 0 = 0）

Question

我正在學習精益證明助手。 https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html的練習是爲自然數定義前驅函數。有人可以幫助我嗎？

Answer 1

你可能熟悉的精益模式匹配或一些功能的編程語言，所以這裏是使用這種機制的解決方案：

open nat 

definition pred : ℕ → ℕ 
| zero  := zero 
| (succ n) := n 

這樣做的另一種方法是使用recursor像這樣：

def pred (n : ℕ) : ℕ := 
    nat.rec_on n 0 (λ p _, p) 

這裏，0就是我們返回如果參數是零，(λ p _, p)是匿名函數有兩個參數：的前身（p）和遞歸調用pred p的結果。匿名函數忽略第二個參數並返回前一個參數。