<!-- Release notes generated using configuration in .github/release.yml at v4.20.0-rc2 --> ## What's Changed * remove the multilingual field from book.toml by @szabgab in https://github.com/lean-ja/lean-by-example/pull/1774 ## New Contributors * @szabgab made their first contribution in https://github.com/lean-ja/lean-by-example/pull/1774 **Full Changelog**: https://github.com/lean-ja/lean-by-example/compare/v4.19.0-rc2...v4.20.0-rc2

<!-- Release notes generated using configuration in .github/release.yml at v4.19.0-rc2 --> **Full Changelog**: https://github.com/lean-ja/lean-by-example/compare/v4.18.0...v4.19.0-rc2

<!-- Release notes generated using configuration in .github/release.yml at v4.18.0 --> **Full Changelog**: https://github.com/lean-ja/lean-by-example/compare/v4.18.0-rc1...v4.18.0

<!-- Release notes generated using configuration in .github/release.yml at v4.18.0-rc1 --> ## Summary * 関数型プログラミング系の説明を充実させた。 * 修飾子というカテゴリを作って、そこに where や termination_by を分類した * mdgen の更新に伴い、多くのページの校正を行った。 ## What's Changed * 帰納型の冒頭の説明がわかりづらい by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1507 * #guard_msgs を消せるようにする by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1508 * 新リファレンスを紹介する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1511 * Logic and Mechanized Reasoning をリンク集に追加する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1512 * scientific computing in Lean をリンク集に追加する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1513 * #eval のエラー説明が誤り by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1514 * macro コマンドの説明変更 by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1518 * 「右結合的な演算」とは？ by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1552 * `show` タクティクがマクロとして定義されていることを確かめる by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1553 * infixl コマンドを紹介する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1554 * infixr コマンドを紹介する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1555 * aconite さんへの謝辞を載せる by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1568 * フィールド記法の説明を「構文」カテゴリに移動させる by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1571 * termination_by は修飾子にカテゴライズする by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1592 * where 句は修飾子として分類する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1594 **Full Changelog**: https://github.com/lean-ja/lean-by-example/compare/v4.17.0-rc1...v4.18.0-rc1

<!-- Release notes generated using configuration in .github/release.yml at v4.17.0-rc1 --> **Full Changelog**: https://github.com/lean-ja/lean-by-example/compare/v4.16.0...v4.17.0-rc1

<!-- Release notes generated using configuration in .github/release.yml at v4.16.0 --> ## What's Changed * Decidable のページのコード例に失敗例がない by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1341 * 不要なnamesapceを使用しない by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1342 * plausibleのコード例にミス by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1343 * Floatのコード例の出所を明示する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1344 * String のページの説明が不親切 by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1347 * `show` タクティクのページに、タクティクではない構文が紹介されている問題の修正 by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1360 * macro のページにタイポ by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1367 * 本書の特色をさらにアピールする by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1369 * `Repr` のルールを反映させて、自作例を修正する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1371 * `unsafe` 修飾子を紹介する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1391 * 構造体の定義の曖昧さ問題 by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1398 * 相対パス表現 `..` を削除する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1399 * 無名コンストラクタの説明を「構文」カテゴリに移動させる by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1402 * Repr のページの文章校正 by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1404 * `private` 修飾子の舞台裏の説明が中途半端 by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1405 * 構造体ではない？ by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1411 * 入れ子リスト(nested list) を簡単に定義する構文を作る、macro_rules 使用例 by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1412 * リスト内包表記を定義する例を紹介する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1413 * macro_rules の使用例として数式を埋め込む例を追加する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1414 * inductive type のスタイル校正 by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1415 * Charのcode pointの説明例をおもしろくする by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1420 * inductive family という用語を使う by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1433 * `inductive` コマンドに対する制約: strictly positive 性 by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1434 * 「出力されたメッセージに～という文字が含まれることを検証するコマンド」を自作する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1435 * `macro` コマンドによって `Macro` 型の項が作られることの検証がコード例に落とし込まれていない by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1436 * strictly positive 性についての補足 by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1439 * strict positivity requirement の説明をより一般的にする by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1441 **Full Changelog**: https://github.com/lean-ja/lean-by-example/compare/v4.16.0-rc2...v4.16.0

<!-- Release notes generated using configuration in .github/release.yml at v4.16.0-rc2 --> ## What's Changed * 何の訳語なのかはっきりさせる by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1298 * `rfl` のコード例で Mathlib を使用しない by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1299 * 構造体に `[ext]` 属性を付与して、`ext` タクティクを利用する例がない by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1304 * `[aesop]` 属性を紹介する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1305 * ライセンスを CC ライセンスにする by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1309 * Functor の説明で、map_const は説明するべき by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1316 * deriving ハンドラがなくても、既にインスタンスがあるものと同じであれば deriving できる by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1317 * `macro` コマンドの例を充実させる by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1320 * macro_rules のコード例が説明文と異なる by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1324 * add_aesop_rules のページにタイポ by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1325 * `ToString` の例が不適切 by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1327 **Full Changelog**: https://github.com/lean-ja/lean-by-example/compare/v4.15.0...v4.16.0-rc2

<!-- Release notes generated using configuration in .github/release.yml at v4.15.0 --> ## What's Changed * `[macro_inline]` 属性を紹介する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1196 * `abbrev` が `@[reducible] def` と同じという主張は根拠がない by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1198 * `qify` のコード例が不適切 by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1200 * zify を紹介する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1214 * 演習問題を削除する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1216 * CI を更新 by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1220 * issue テンプレートを消す by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1221 * `#test` コマンドを紹介する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1222 * `push_cast` を紹介する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1223 * show_term の項目を独立させる by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1233 * `hint` タクティクの説明が不完全 by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1235 * `ring` タクティクを新しい型に対して使う方法を示す by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1245 * ring タクティクの説明の更新 by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1248 * refine は、自明な部分を手軽に片すのにも使える by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1251 * `Nat` を紹介する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1253 * linter エラーが設定を貫通する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1255 * `use` タクティクを紹介する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1257 * section の説明に「スコープ」という語を使わない by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1260 * 単独で執筆していることを明記する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1264 * 「宣言的コマンド」「対話的コマンド」という用語が一般的でないことを注意する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1266 * 修飾子を宣言的コマンドから独立させる by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1267 * `private` の例を `protected` のページに置かない by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1271 * 複数ファイルからなる記事の扱いについて by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1272 * `List` がモナドであることを説明する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1276 * version update by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1277 * 三項演算のままになってる by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1279 * `termination_by` はトップレベルコマンドではない by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1280 * 暗黙の引数 `{x y : A}` を紹介する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1284 * `by` はタクティクではないことを注意する by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1286 * lychee-action が動作していない by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1290 * lychee のバージョンを敢えて下げる by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1291 * mdgen のバグで `#lint` コマンドの出力をアサートできていない by @Seasawher in https://github.com/lean-ja/lean-by-example/pull/1293 **Full Changelog**: https://github.com/lean-ja/lean-by-example/compare/v4.15.0-rc1...v4.15.0