v4.14.0-rc2

What's Changed

• sorry の舞台裏を説明する by @Seasawher in #1048
• Float が仮数と指数で表現されていることを示す by @Seasawher in #1050
• Bool を紹介する by @Seasawher in #1051
• Functor 型クラスを紹介する by @Seasawher in #1053
• HAdd 型クラスを紹介する by @Seasawher in #1055
• Array 型を紹介する by @Seasawher in #1062
• 「index in target's type is not a variable」エラーはいつ起こるのか？ by @Seasawher in #1064
• induction ... generalizing 構文とその制約を紹介する by @Seasawher in #1067
• Bump lycheeverse/lychee-action from 2.0.2 to 2.1.0 by @dependabot in #1071
• バージョン更新 by @Seasawher in #1072

Full Changelog: v4.13.0...v4.14.0-rc2

v4.13.0

What's Changed

• autoImplicit オプションを紹介する by @Seasawher in #940
• warning が出ないようにする by @Seasawher in #944
• /-! .. -/ を使用しない by @Seasawher in #946
• flexible リンタの警告を消す by @Seasawher in #947
• windows build も lean action を使う by @Seasawher in #948
• warning がないことをCIで検証する by @Seasawher in #951
• mdbook 用の markdown ファイルを格納するディレクトリの名前を booksrc に変える by @Seasawher in #952
• ディレクトリ名変更: Examples → LeanByExample by @Seasawher in #953
• ディレクトリ構成変更 by @Seasawher in #954
• CI の構成を簡単にする by @Seasawher in #956
• リンターオプションを追加する by @Seasawher in #959
• linter.flexible を紹介する by @Seasawher in #960
• flexible リンタの警告が消えない問題の修正 by @Seasawher in #961
• option のデフォルト値を取得する関数 by @Seasawher in #966
• relaxedAutoImplicit オプションを紹介する by @Seasawher in #968
• citation 指定にカンマがない by @Seasawher in #973
• Reservoir 用のメタデータを追加する by @Seasawher in #975
• 帰納型の族の話をよくあるエラーではなく帰納型の例として紹介する by @Seasawher in #977
• 帰納的命題を考えるメリットを説明する by @Seasawher in #979
• aesop の destructビルダーについて説明する by @Seasawher in #985
• 帰納法の説明を修正し、丁寧にする by @Seasawher in #992
• mathlib4-tactics のリンク変更 by @Seasawher in #998
• Mathlib のバージョン更新 by @Seasawher in #1005
• #print で既存の帰納型を紹介しない by @Seasawher in #1008
• List.fold の記述の誤り by @Seasawher in #1012
• オプションの名前をフルネームにする by @Seasawher in #1013
• tauto タクティクの説明で、命題論理を強調する by @Seasawher in #1016
• aesop タクティクの説明方法 by @Seasawher in #1044
• simp_all を独立したタクティクとして紹介する by @Seasawher in #1045

Full Changelog: v4.13.0-rc3...v4.13.0

v4.13.0-rc3

What's Changed

• 浮動小数点数をなるべく正確に表示させる方法 by @Seasawher in #928
• <;> の名前は？seqFocusでよいのか？ by @Seasawher in #931
• hygine というオプションを紹介する by @Seasawher in #935
• 「帰納型」や「構造体」もリンクにする by @Seasawher in #936
• hygiene の綴りのミス by @Seasawher in #938

Full Changelog: v4.12.0...v4.13.0-rc3

v4.12.0

Summary

このリリースから PDF 版は生成しないことにした。

What's Changed

• lake run build の実行が遅いので代替手段を用意する by @Seasawher in #766
• 排中律と De Morgan の問題の Heyting 代数の問題への差し替え by @Seasawher in #767
• 不要な仮定を削除する by @Seasawher in #768
• aesop に追加の補題を渡す方法を説明する by @Seasawher in #781
• 印刷ボタンが正常に機能しない by @Seasawher in #782
• PDF 版を生成しない by @Seasawher in #788
• rw はローカル変数の展開は行わない by @Seasawher in #789
• inductive datatype parameter mismatch エラーはなぜ起こる？ by @Seasawher in #791
• elab コマンド使用例：tada タクティク by @Seasawher in #792
• Heyting 代数の問題文を微修正 by @Seasawher in #797
• Cantor の対関数についての証明は出典を示す by @Seasawher in #802
• 自動更新PRにラベルを貼り、リリースノートから自動的に除外されるようにする by @Seasawher in #796
• lean searchをリンクチェック対象に戻す by @Seasawher in #808
• [inherit_doc] を紹介する by @Seasawher in #815
• @[match_pattern] 属性を紹介する by @Seasawher in #817
• 属性の名前は [ ] で囲うスタイルにする by @Seasawher in #818
• precedence と priority を明確に分ける by @Seasawher in #821
• 目次のネストを1段階に固定する by @Seasawher in #832
• 見出しを展開しない by @Seasawher in #834
• 目次の順番の入れ替え by @Seasawher in #840
• 属性を [ ] で囲っていない箇所がある by @Seasawher in #843
• 証明無関係の表記揺れ by @Seasawher in #844
• タグ🏷️機能を試験的に実装する by @Seasawher in #853
• テスト: iPadおよびiPhoneのsafariではページごとの実行ボタンが動作しない by @Seasawher in #857
• handlebars のフォーマットを行う by @Seasawher in #859
• pagetoc.js 内でCSSを挿入しない by @Seasawher in #863
• GetElem のページに、証明付きアクセスも紹介する by @Seasawher in #867
• Biome で js ファイルのフォーマットなどを行う by @Seasawher in #868
• String と文字列補完を紹介する by @Seasawher in #871
• norm_cast タクティクを紹介する by @Seasawher in #876
• precedence は「（パースの）優先度」ではなくて「（パースの）優先順位」と訳す by @Seasawher in #880
• 全射/単射の分裂 by @Seasawher in #884
• Cantorの定理の難易度調整 by @Seasawher in #885
• Discord へのリンクをトップバーに移動させる by @Seasawher in #892
• 一瞬 Suggest an edit ボタンが表示される問題を修正する by @Seasawher in #893
• Leanの公式ブログをリンク集に追加する by @Seasawher in #894
• atttibute [coe]でインフォビュー上での表示を↑に換える by @Seasawher in #898
• [default_instance] 属性を紹介する by @Seasawher in #900
• インスタンス優先度と [default_instance] 属性の違いをコード例で示す by @Seasawher in #902
• [norm_cast] 属性を紹介する by @Seasawher in #903
• Char 型を紹介する by @Seasawher in #904
• 強調された文字の色を変える by @Seasawher in #907
• 強調された文字の色を変えない by @Seasawher in #909
• List 型を紹介する by @Seasawher in #911
• deriving は def に対しても使える by @Seasawher in #916
• List.foldl を紹介する by @Seasawher in #918
• List の高階関数についての記述を追加する by @Seasawher in #920
• List.foldl と List.foldr の説明が不適当 by @Seasawher in #924

Full Changelog: v4.12.0-rc1...v4.12.0

v4.12.0-rc1

Summary

Cantor の対関数が全単射であることを示せという問題を追加しました。

What's Changed

• app_unexpander の説明を修正する by @Seasawher in #749
• Cantor の対関数を演習問題にする by @Seasawher in #752
• with_reducible の使用例 by @Seasawher in #753

Full Changelog: v4.11.0...v4.12.0-rc1

v4.11.0

Summary

• 演習問題というセクションを追加しました。これは、MIL に相当する内容を拾っていくことを目指しています。

• メタプロ関連のコマンドの説明を充実させました。

What's Changed

• コマンド: macro_rules を紹介する by @Seasawher in #624
• syntax コマンドを紹介する by @Seasawher in #626
• syntax コマンドの優先順位の指定が必要な例 by @Seasawher in #629
• workflow更新 by @Seasawher in #631
• 演習問題を追加する by @Seasawher in #632
• ヒントが初期状態で見えないようにする by @Seasawher in #642
• 演習問題と解答の同期が保たれない by @Seasawher in #643
• CONTRIBUTING 修正 by @Seasawher in #648
• 商の公理から関数外延性を導く証明を丁寧にする by @Seasawher in #651
• 騎士と悪党の論理パズルにおける問題文の形式化がおかしい by @Seasawher in #654
• 騎士と悪党のパズルで、最後に排中律を使用していないことをチェックする by @Seasawher in #656
• #print axioms の舞台裏: 選択原理 choice を使っているかチェックするコマンド by @Seasawher in #657
• Cantorの定理を演習問題に追加する by @Seasawher in #666
• expand_tactic と expand_command を統一する by @Seasawher in #675
• 宣言的コマンド: declare_syntax_cat を紹介する by @Seasawher in #676
• runCmd の実装方法を変更し、文字列を渡せばいいようにする by @Seasawher in #685
• 開発: DevContainer 環境に mdbook-admonish を追加する by @Seasawher in #691
• Diaconescu の定理の証明の修正 by @Seasawher in #692
• 演習問題はLeanでビルドしない by @Seasawher in #693
• #time コマンドで計測されるLeanの計算時間はなぜ遅いのか by @Seasawher in #694
• 演習問題に autoImplicit false を追加する by @Seasawher in #707
• sync ワークフローの修正とテスト実行 by @Seasawher in #710
• protected は帰納型のコンストラクタにも使用できる by @Seasawher in #711
• リファクタ: left と right を別々に紹介する by @Seasawher in #712
• windows build は PR 時に走らせない by @Seasawher in #717
• 演習問題フォルダの場所を変える by @Seasawher in #719
• <;> を見出し語にする by @Seasawher in #720
• 含意の定義の正当性の問題を、排中律を使用しない問題として書き直す by @Seasawher in #726
• simp_rw の使い方と rw の制約 by @Seasawher in #727
• simp at * が通らず simp_all が通る例 by @Seasawher in #728
• 型クラス紹介: GetElem 型クラス by @Seasawher in #729
• 追記:帰納型とは何か, Lean の型システムの概略について by @Seasawher in #731
• 属性リストへのリンクを追加する by @Seasawher in #732
• app_unexpander 属性を紹介する by @Seasawher in #734
• 自動マージPRを作成する by @Seasawher in #735
• checkout は不要なので削除する by @Seasawher in #736
• job の名前を明確にする by @Seasawher in #737
• protected の用途を注釈する by @Seasawher in #738
• protected のコードの修正 by @Seasawher in #739
• Lean のバージョン更新 by @Seasawher in #744

Full Changelog: v4.11.0-rc2...v4.11.0

v4.11.0-rc2

Summary

検索の挙動が直観に反していて、見出し語を探すのが面倒だったのを修正しました。

What's Changed

• Prop の説明が中途半端だったので改定 by @Seasawher in #612
• 検索で見出し語が一番上に出てこないことがある by @Seasawher in #616

Full Changelog: v4.11.0-rc1...v4.11.0-rc2

v4.11.0-rc1

Summary

PC など広いディスプレイで閲覧したとき、右側に目次を自動生成して表示させるようになりました。
また、Lean Search というツールをリンク集に追加しました。
内容面では、Prop の非可述性や Type の可述性など Lean の理論面に関する内容を強化しました。

What's Changed

• 属性: csimp 属性 by @Seasawher in #556
• リンク集更新 by @Seasawher in #557
• ページ内目次を表示させる by @Seasawher in #566
• axiom: なぜ商の公理だけが特別なのか by @Seasawher in #569
• 証明無関係の説明に誤り by @Seasawher in #576
• Prop の非可述性を説明する by @Seasawher in #577
• Type : Type と仮定すると矛盾が生じること by @Seasawher in #580
• v4.11.0-rc1 に更新する by @Seasawher in #590

Full Changelog: v4.10.0...v4.11.0-rc1

v4.10.0

重要な変更

PDFを生成するようになり、特定のバージョンの本書を参照しやすくなった。
ただし、PDF版を読むのは非推奨。あくまで参照のためだけのものである。

これ以降のリリースにはPDFを添付していく。

What's Changed

• feat: Windows 上でビルドするCIを追加する by @Seasawher in #470
• macro コマンドを紹介する by @Seasawher in #472
• DevContainer の構成を CI でチェックする by @Seasawher in #481
• 句読点を 、 と 。 に統一する by @Seasawher in #487
• タクティク: positivity を紹介する by @Seasawher in #488
• fix: 選択原理の説明を修正する by @Seasawher in #499
• doc: 句読点ルールに例外を設ける by @Seasawher in #500
• feat: フィールド記法を紹介する by @Seasawher in #501
• OfNat 型クラスを紹介する by @Seasawher in #503
• abbrevを「別名」と訳すのを止める by @Seasawher in #514
• Prop からは Prop しか取り出せない by @Seasawher in #507
• fix: 不適切なカンマ by @Seasawher in #518
• feat:「この処理は ... ミリ秒以内に終わる」という性能テストを書く by @Seasawher in #519
• feat: set_option 構文を紹介する by @Seasawher in #520
• feat: outParam を紹介する by @Seasawher in #521
• doc: 各カテゴリの分類基準を明記する by @Seasawher in #524
• feat: #reduce コマンドを紹介する by @Seasawher in #525
• Decidable を紹介する by @Seasawher in #528
• feat: hygiene macro について説明する例 by @Seasawher in #529
• refactor: rcases を cases から独立させる by @Seasawher in #530
• mdbook-pdf を利用して PDF を生成する by @Seasawher in #513
• 見出しの中でインラインコードを使用しない by @Seasawher in #540
• doc: 引用方法を指定する by @Seasawher in #541
• ファイルの命名規則を更新する by @Seasawher in #545
• feat: 選択原理等から排中律を証明する例を追加する by @Seasawher in #546
• feat: attribute の削除は常にローカルであることを示す例 by @Seasawher in #547
• 属性を紹介する by @Seasawher in #553

Full Changelog: v4.10.0-rc2...v4.10.0

v4.10.0-rc2

重要な変更

コマンドとタクティクだけでなく，型クラスも紹介するようになった．

What's Changed

• linarith に引数で補題を渡す例を紹介する by @Seasawher in #434
• field_simp は順序を扱えない by @Seasawher in #435
• notation のコード例における優先順位修正 by @Seasawher in #436
• コマンド紹介: infix を紹介する by @Seasawher in #437
• infix コマンドは左結合でも右結合でもないことを明記する by @Seasawher in #439
• Updates available and ready to merge. by @github-actions in #440
• コマンド紹介：opaque を紹介する by @Seasawher in #447
• Updates available and ready to merge. by @github-actions in #449
• fix: 宣言的コマンドの説明で「構文」と呼んでいるのを「コマンド」に統一する by @Seasawher in #450
• feat: prefix コマンドを紹介する by @Seasawher in #451
• feat: ロゴ画像を README に追加する by @Seasawher in #453
• feat: postfix コマンドを紹介する by @Seasawher in #454
• fix: local と scoped が使えるコマンドを検証する by @Seasawher in #456
• feat: 旧Lean by Exampleから型クラスの記事を移設する by @Seasawher in #459
• feat: Repr を deriving を使わずに実装する例を示す by @Seasawher in #461
• v4.10.0-rc2 に更新する by @Seasawher in #468

Full Changelog: v4.10.0-rc1...v4.10.0-rc2