![](https://cdn-ak-scissors.b.st-hatena.com/image/square/a6e2159f1fd8b64a33c1ea40a937c3a66a38819c/height=288;version=1;width=512/https%3A%2F%2Fres.cloudinary.com%2Fzenn%2Fimage%2Fupload%2Fs--BJItFo4z--%2Fc_fit%252Cg_north_west%252Cl_text%3Anotosansjp-medium.otf_55%3ATAPL%2525E3%252581%2525A8Lean%2525E3%252581%2525AE%2525E5%252590%25258C%2525E6%252599%252582%2525E5%252585%2525A5%2525E9%252596%252580%2525E3%252581%2525AE%2525E3%252582%2525B9%2525E3%252582%2525B9%2525E3%252583%2525A1%252520%2525E4%2525BA%252588%2525E5%252591%25258A%2525E7%2525B7%2525A8%252528%2525E7%2525B7%2525A0%2525E5%252588%252587%2525E3%252581%2525AB%2525E6%252595%252597%2525E5%25258C%252597%2525E3%252581%252597%2525E3%252581%2525BE%2525E3%252581%252597%2525E3%252581%25259F%252529%252Cw_1010%252Cx_90%252Cy_100%2Fg_south_west%252Cl_text%3Anotosansjp-medium.otf_37%3Aebi_chan%252Cx_203%252Cy_121%2Fg_south_west%252Ch_90%252Cl_fetch%3AaHR0cHM6Ly9zdG9yYWdlLmdvb2dsZWFwaXMuY29tL3plbm4tdXNlci11cGxvYWQvYXZhdGFyLzcxMDMyZmVmYTguanBlZw%3D%3D%252Cr_max%252Cw_90%252Cx_87%252Cy_95%2Fv1627283836%2Fdefault%2Fog-base-w1200-v2.png)
エントリーの編集
![loading...](https://b.st-hatena.com/bdefb8944296a0957e54cebcfefc25c4dcff9f5f/images/v4/public/common/loading@2x.gif)
エントリーの編集は全ユーザーに共通の機能です。
必ずガイドラインを一読の上ご利用ください。
TAPLとLeanの同時入門のススメ 予告編(締切に敗北しました)
記事へのコメント0件
- 注目コメント
- 新着コメント
このエントリーにコメントしてみましょう。
注目コメント算出アルゴリズムの一部にLINEヤフー株式会社の「建設的コメント順位付けモデルAPI」を使用しています
![アプリのスクリーンショット](https://b.st-hatena.com/bdefb8944296a0957e54cebcfefc25c4dcff9f5f/images/v4/public/entry/app-screenshot.png)
- バナー広告なし
- ミュート機能あり
- ダークモード搭載
関連記事
TAPLとLeanの同時入門のススメ 予告編(締切に敗北しました)
この記事は定理証明支援系 Advent Calendar 2023 の3日目の記事です。 2日目は @elpinal さんの Isabell... この記事は定理証明支援系 Advent Calendar 2023 の3日目の記事です。 2日目は @elpinal さんの Isabelle/HOLで位相空間論の初歩を証明した でした。 注意 この記事は未完成のまま投稿されています。(筆者が締切に敗北したため) 投稿前にレビューをもらったところまだまだ説明が足りない部分が見つかったので、頑張って完成度を上げていく所存です。 あと、かなりの長編になりそうで本編は4~5回に分けて投稿することになるかも。 TAPLの3章をLeanで形式化したコードについてはここから参照できます。この内容が理解できるところまで解説するのが目標です。 この記事は以下のような人を想定読者としています。怖くないよ! Python、Java、TypeScriptなどの言語は使えるが、OCamlやHaskellのような関数型言語には馴染みがない 大学で習うような高度な数