v4.13.0
What's Changed
autoImplicit
オプションを紹介する by @Seasawher in #940- warning が出ないようにする by @Seasawher in #944
/-!
..-/
を使用しない by @Seasawher in #946flexible
リンタの警告を消す 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 #960flexible
リンタの警告が消えない問題の修正 by @Seasawher in #961option
のデフォルト値を取得する関数 by @Seasawher in #966relaxedAutoImplicit
オプションを紹介する 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