Mathmatics In Lean4の第5章 初等数論の2つ目の話題は帰納法と再帰です。自然数では定義が帰納的であること(自然数型は帰納型であること)を知ります。 inductive Nat | zero : Nat | succ (n : Nat) : Nat この意味は、0はNat型、Nat型の要素を1つとって…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。