プログラミング言語であるとともに定理証明支援系でもある Lean 言語と,その主要なライブラリの使い方を豊富なコード例とともに解説した資料です.
[!WARNING] 本書は現在開発中であり,各ページのURLが予告なく変更され,リダイレクトも設定されないということがあり得ます.リンク切れを避けるには,個別ページではなくトップページにリンクを張るようにしてください.
誤りの指摘,編集の提案や寄稿を歓迎いたします.この GitHubリポジトリに issue や Pull Request を開いてください.
,
.
を使用します.foo
に対して,目次の中での記事の名前は foo: (日本語による一言説明)
とします.可能な限り1行に収まるようにしてください.src/SUMMARY.md
の内の記事は,カテゴリごとにアルファベット昇順に並べてください.VSCode だと Tyriar.sort-lines という拡張機能があって,並び替えを自動で行うことができます.lake run build
コマンドを実行すれば markdown の生成と mdbook build
が一括実行されます.Examples
配下に配置します.「エラーになる例」を紹介したいときであっても try
や #guard_msgs
や fail_if_success
などを使ってコンパイルが通るようにしてください.コード例が正しいかチェックする際にその方が楽だからです.Thank you for your interest in translating this book! 😄 But please note that we are currently not accepting translations of this book because this book is still under development! No content is stable yet.
このプロジェクトは Proxima Technology 様よりご支援を頂いています.
Proxima Technology(プロキシマテクノロジー)は数学の社会実装を目指し, その⼀環としてモデル予測制御の民主化を掲げているAIスタートアップ企業です.数理科学の力で社会を変えることを企業の使命としています.