演習問題

このセクションでは、演習問題を扱います。ぜひ新しいパズルゲームだと思って挑戦してみてください。

🎮 遊び方

問題は、前提となるライブラリや知識が少なく、難易度が低いと思われる順に並べてあります。興味があるものから挑戦してみましょう。

解き始めるための最も簡単で手軽な方法は、Lean 4 Playground を使う方法です。各ページの右上に というボタンがあるので、これをクリックしてください。Lean 4 Playground のページに移動し、そのままブラウザ上で演習問題を解き始めることができます。

あるいは、Codespace を開き、LeanByExample/Tutorial/Exercise ディレクトリの中にある該当ファイルを開いてもよいです。

お使いの PC に Lean をインストール済みであれば、このリポジトリをクローンして VSCode で開いてください。

❓ どうしてもわからないとき

時間をかけて考えてみてください。著者は簡単な問題をたくさん解くのではなく、おもしろい問題にじっくり取り組んだ方が学びは大きいと信じています。どの問題も、本書のレファレンス部分を参照しつつ試行錯誤をすれば自力で解けることを目指して作っています。

しかし、自力で解いた後に解答を見るのは構いません。解答は LeanByExample/Tutorial/Solution ディレクトリに置いてあります。