Skip to content

v4.11.0

Compare
Choose a tag to compare
@Seasawher Seasawher released this 02 Sep 15:12
· 393 commits to main since this release
359b20b

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