{"author_name":"jurupapa","image_url":"https://cdn-ak.f.st-hatena.com/images/fotolife/j/jurupapa/20240403/20240403223351.jpg","blog_title":"Maxima \u3067\u7db4\u308b\u6570\u5b66\u306e\u65c5","blog_url":"https://maxima.hatenablog.jp/","title":"-Lean4\u306e\u304a\u52c9\u5f37\u3000\u5e30\u7d0d\u6cd5\u3068\u518d\u5e30","categories":["\u6570\u5b66"],"provider_url":"https://hatena.blog","width":"100%","published":"2024-04-03 23:46:32","provider_name":"Hatena Blog","version":"1.0","height":"190","author_url":"https://blog.hatena.ne.jp/jurupapa/","url":"https://maxima.hatenablog.jp/entry/2024/04/03/234632","type":"rich","description":"Mathmatics In Lean4\u306e\u7b2c5\u7ae0 \u521d\u7b49\u6570\u8ad6\u306e\uff12\u3064\u76ee\u306e\u8a71\u984c\u306f\u5e30\u7d0d\u6cd5\u3068\u518d\u5e30\u3067\u3059\u3002\u81ea\u7136\u6570\u3067\u306f\u5b9a\u7fa9\u304c\u5e30\u7d0d\u7684\u3067\u3042\u308b\u3053\u3068\uff08\u81ea\u7136\u6570\u578b\u306f\u5e30\u7d0d\u578b\u3067\u3042\u308b\u3053\u3068\uff09\u3092\u77e5\u308a\u307e\u3059\u3002 inductive Nat | zero : Nat | succ (n : Nat) : Nat \u3053\u306e\u610f\u5473\u306f\u30010\u306fNat\u578b\u3001Nat\u578b\u306e\u8981\u7d20\u3092\uff11\u3064\u3068\u3063\u3066n\u3068\u3059\u308b\u3068succ n\u3082Nat\u578b\u3067\u3059\u3002\u305d\u3057\u3066succ n=0\u3068\u306a\u308b\u3088\u3046\u306an\u306f\u3042\u308a\u307e\u305b\u3093\u3002\u3061\u306a\u307f\u306bsucc n\u306fn+1\u3068\u3082\u66f8\u304b\u308c\u307e\u3059\u3002 \u6b21\u306b\u3053\u306e\u578b\u306e\u4e0a\u3067\u968e\u4e57\u95a2\u6570\u3092\u518d\u5e30\u7684\u306b\u5b9a\u7fa9\u3057\u307e\u3059\u3002 def fac : \u2115 \u2192 \u2115 | 0 => 1 | n + 1 => (n + 1) * fac \u2026","html":""}