Leanの自然数の先行関数（pred 0 = 0）を定義する

Question

私はLean proof assistantを学習しています。 https://leanprover.github.io/theorem_proving_in_lean/inductive_types.htmlのエクササイズは、自然数の先行関数を定義することです。誰かが私を助けることができますか？

open nat 

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

ので、同じようrecursorを使用しているこれを行う別の方法：あなたはので、ここで、おそらくリーンまたはいくつかの関数型プログラミング言語からパターンマッチングに精通している

Answer 1

は、このメカニズムを使用するソリューションです

の前身（ p）： ここ

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

、0は、引数がゼロであると(λ p _, p) 2つの引数を取る匿名関数であるならば、我々は返すものです再帰呼び出しpred pの結果を返します。無名関数は2番目の引数を無視し、先行操作を返します。