Merge branch 'update'

Seasawher · Seasawher · commit af530228fba2 · 2025-02-04T21:18:11.000+09:00
diff --git a/LeanByExample/Declarative/Class.lean b/LeanByExample/Declarative/Class.lean
@@ -60,7 +60,6 @@ def instMonoid'Nat : Monoid' Nat where
 
 /- `self : Monoid' α` が暗黙の引数ではなく明示的な引数なので、型クラスのように書くことはできません。-/
 
-#guard_msgs (drop warning) in --#
 #check_failure (Monoid'.e : Nat)
 
 /- しかし、インスタンスを引数として渡せば、型クラスのように `Nat` の要素を取り出すことができます。-/
diff --git a/LeanByExample/Declarative/DeclareSyntaxCat.lean b/LeanByExample/Declarative/DeclareSyntaxCat.lean
@@ -41,11 +41,8 @@ syntax "{" binder "|" term "}" : term
 
 -- 合法な構文として認識される
 -- 実装は与えていないのでエラーにはなる
-#guard_msgs (drop warning) in --#
 #check_failure { x | x = 0}
-#guard_msgs (drop warning) in --#
 #check_failure { x : Nat | x > 0 }
-#guard_msgs (drop warning) in --#
 #check_failure { x ∈ T | x = 0}
 
 /-- `{x : T | P x}` と `{x ∈ T | P x}` の形の式を `setOf` の式に変換する -/
diff --git a/LeanByExample/Declarative/Export.lean b/LeanByExample/Declarative/Export.lean
@@ -16,7 +16,6 @@ namespace N -- export コマンドが実行される名前空間
 
   -- foo は名前空間 Sample 上にあるので、
   -- 短い名前ではアクセスできない
-  #guard_msgs (drop warning) in --#
   #check_failure foo
   #check Sample.foo
 
@@ -30,7 +29,6 @@ end N
 
 -- 名前空間 `N` の外部からアクセスするには、
 -- 普通はフルネームが必要
-#guard_msgs (drop warning) in --#
 #check_failure N.bar
 #check N.Sample.bar
 
diff --git a/LeanByExample/Declarative/Infix.lean b/LeanByExample/Declarative/Infix.lean
@@ -22,7 +22,6 @@ infix:51 " strong " => Nat.add
 -- したがってエラーになる
 infix:49 " weak " => Nat.add
 
-#guard_msgs (drop warning) in --#
 #check_failure 1 + 2 weak 3 = 6
 
 /- `infix` で定義される記法は左結合でも右結合でもなく、必ず括弧が必要です。-/
diff --git a/LeanByExample/Declarative/Instance.lean b/LeanByExample/Declarative/Instance.lean
@@ -12,7 +12,6 @@ structure Point (α : Type) where
 def origin : Point Int := { x := 0, y := 0 }
 
 -- 数値のように足し算をすることはできない
-#guard_msgs (drop warning) in --#
 #check_failure (origin + origin)
 
 /-- 平面上の点の足し算ができるようにする -/
@@ -57,7 +56,6 @@ instance {n : Nat} [OfNat Even n] : OfNat Even (n + 2) where
 #guard (2 : Even) = Even.succ Even.zero
 
 -- 奇数については OfNat の実装はない
-#guard_msgs (drop warning) in --#
 #check_failure (3 : Even)
 
 /- なお、インスタンス連鎖の回数には上限があります。-/
@@ -66,7 +64,6 @@ instance {n : Nat} [OfNat Even n] : OfNat Even (n + 2) where
 #eval (254 : Even)
 
 -- 上限を超えてしまった
-#guard_msgs (drop warning) in --#
 #check_failure (256 : Even)
 
 /-
@@ -75,7 +72,6 @@ instance {n : Nat} [OfNat Even n] : OfNat Even (n + 2) where
 -/
 
 -- `List` 同士を足すことはできない
-#guard_msgs (drop warning) in --#
 #check_failure [1] + [2]
 
 -- インスタンスを宣言する
@@ -91,5 +87,4 @@ def instListAdd {α : Type} : Add (List α) where
 attribute [-instance] instListAdd
 
 -- リスト同士を足すことができなくなった
-#guard_msgs (drop warning) in --#
 #check_failure [1] + [2]
diff --git a/LeanByExample/Declarative/MacroRules.lean b/LeanByExample/Declarative/MacroRules.lean
@@ -117,7 +117,6 @@ end Set
 syntax "{{" term,* "}}" : term
 
 -- `syntax` コマンドは記法の解釈方法を決めていないので、エラーになる
-#guard_msgs (drop warning) in --#
 #check_failure {{2, 3}}
 
 -- 集合の波括弧記法をどう解釈するかのルールを定める
@@ -150,7 +149,6 @@ namespace NestedList
   syntax "《" term,* "》" : term
 
   -- `syntax` コマンドは記法の解釈方法を決めていないので、エラーになる
-  #guard_msgs (drop warning) in --#
   #check_failure 《1, 《2, 3》, 4》
 
   macro_rules
@@ -186,11 +184,8 @@ namespace ListComp
   syntax "[" term " | " compClause,* "]" : term
 
   -- `syntax` コマンドは記法の解釈方法を決めていないので、エラーになる
-  #guard_msgs (drop warning) in --#
   #check_failure [x | for x in [1, 2, 3, 4, 5]]
-  #guard_msgs (drop warning) in --#
   #check_failure [x | if x < 2]
-  #guard_msgs (drop warning) in --#
   #check_failure [x | for x in [1, 2, 3], if x < 2]
 
   macro_rules
@@ -252,11 +247,8 @@ namespace Expr
   syntax:max "(" expr ")" : expr
 
   -- `syntax` コマンドは記法の解釈方法を決めていないので、エラーになる
-  #guard_msgs (drop warning) in --#
   #check_failure expr!{1 + 2}
-  #guard_msgs (drop warning) in --#
   #check_failure expr!{1 * 2}
-  #guard_msgs (drop warning) in --#
   #check_failure expr!{(1 + 2) * 3}
 
   macro_rules
diff --git a/LeanByExample/Declarative/Namespace.lean b/LeanByExample/Declarative/Namespace.lean
@@ -20,7 +20,6 @@ namespace Nat
 end Nat
 
 -- 名前空間の外に出ると、短い名前ではアクセスできない
-#guard_msgs (drop warning) in --#
 #check_failure isEven
 
 -- フルネームならアクセスできる
diff --git a/LeanByExample/Declarative/Notation.lean b/LeanByExample/Declarative/Notation.lean
@@ -131,7 +131,6 @@ set_option pp.mvars false
 
 -- 等号（パース優先順位 50）より優先順位が低いという問題でエラーになる
 -- 上では60で定義しているのに、なぜ？
-#guard_msgs (drop warning) in --#
 #check_failure true ⊕ true = false
 
 -- 括弧を付けるとエラーにならない
@@ -158,7 +157,6 @@ local macro_rules | `($x ⊕ $y) => `(xor $x $y)
 #guard false ⊕ false = false
 
 -- 上書きされたので、 Sum の意味で ⊕ を使うことはできなくなった
-#guard_msgs (drop warning) in --#
 #check_failure Nat ⊕ Fin 2
 end --#
 
diff --git a/LeanByExample/Declarative/Open.lean b/LeanByExample/Declarative/Open.lean
@@ -11,7 +11,6 @@ namespace Hoge
 end Hoge
 
 -- 名前空間の外からだと `foo` という短い名前が使えない
-#guard_msgs (drop warning) in --#
 #check_failure foo
 
 section
@@ -23,7 +22,6 @@ section
 end
 
 -- セクションが終わると再び短い名前は使えなくなる
-#guard_msgs (drop warning) in --#
 #check_failure foo
 
 /- ## 入れ子になった名前空間
diff --git a/LeanByExample/Declarative/ProofWanted.lean b/LeanByExample/Declarative/ProofWanted.lean
@@ -19,5 +19,4 @@ theorem another_result : n + 0 = n := by sorry
 #check another_result
 
 -- proof_wanted で宣言した定理は参照できない
-#guard_msgs (drop warning) in --#
 #check_failure result
diff --git a/LeanByExample/Declarative/Section.lean b/LeanByExample/Declarative/Section.lean
@@ -23,7 +23,6 @@ section
 end
 
 -- `section` の外に出ると無効になる
-#guard_msgs (drop warning) in --#
 #check_failure a
 
 /-
@@ -38,7 +37,6 @@ section
 end
 
 -- `end` 以降は無効になる
-#guard_msgs (drop warning) in --#
 #check_failure choice
 
 /- 次は `set_option` の有効範囲を区切る例です。 -/
@@ -88,10 +86,8 @@ section parent
   end child
 
   -- child セクションの外なので無効
-  #guard_msgs (drop warning) in --#
   #check_failure b
 end parent
 
 -- parent セクションの外なので無効
-#guard_msgs (drop warning) in --#
 #check_failure a
diff --git a/LeanByExample/Declarative/Structure.lean b/LeanByExample/Declarative/Structure.lean
@@ -123,7 +123,6 @@ inductive Point' (α : Type) : Type where
 /- アクセサ関数が自動的に作られませんが、自分で作ることができます。-/
 
 -- アクセサ関数が利用できない
-#guard_msgs (drop warning) in --#
 #check_failure Point'.x
 
 /-- 自前で定義した `Point'` へのフィールドへのアクセサ -/
@@ -139,12 +138,7 @@ def Point'.x {α : Type} (p : Point' α) : α :=
 /- 波括弧記法は `structure` コマンドで定義された型でなければ使用できないようです。 -/
 
 -- 波括弧記法は使用できない
-/--
-warning: invalid {...} notation, structure type expected
-  Point' Int
--/
-#guard_msgs in
-  #check_failure { x := 1, y := 2 : Point' Int}
+#check_failure { x := 1, y := 2 : Point' Int}
 
 /- ### 用途
 この `structure` コマンドの代わりに `inductive` コマンドを用いる方法は、定義しようとしている構造体が命題をパラメータに持っているときに必要になります。[`Prop` の Large Elimination が許可されていない](#{root}/Type/Prop.md#NoLargeElim)ことにより、この場合はアクセサ関数が生成できないので `structure` コマンドが使用できず、エラーになります。 -/
diff --git a/LeanByExample/Declarative/Syntax.lean b/LeanByExample/Declarative/Syntax.lean
@@ -45,16 +45,10 @@ local macro_rules
 -- メタ変数の番号を表示しない
 set_option pp.mvars false
 
--- `Nat` と `Prop` を足すことはできないというエラーメッセージ。
--- `1 + (1 = 2)` だと認識されてしまっているようだ。
-/--
-warning: failed to synthesize
-  HAdd Nat Prop ?_
-Additional diagnostic information may be available
-using the `set_option diagnostics true` command.
--/
-#guard_msgs (warning) in
-  #check_failure (1 + 1 = 2 as Nat)
+-- `1 + (1 = 2)` だと認識されてしまっている
+/-- info: 1 + (1 = 2) : ?_ -/
+#guard_msgs (info, drop error) in
+  #check (1 + 1 = 2 as Nat)
 
 end --#
 /- **パース優先順位(parsing precedence)** を設定することで、どの構文から順に解釈されるかを指定することができ、問題を修正できることがあります。このあたりは [`notation`](./Notation.md) コマンドと同様です。 -/
diff --git a/LeanByExample/Diagnostic/CheckFailure.lean b/LeanByExample/Diagnostic/CheckFailure.lean
@@ -3,13 +3,10 @@
 -/
 
 -- 自然数と文字列を足すことはできない
-#guard_msgs (drop warning) in --#
 #check_failure 1 + "hello"
 
 -- `1 = 2` を `rfl` で証明することはできない
-#guard_msgs (drop warning) in --#
 #check_failure (by rfl : 1 = 2)
 
 -- `1 + 4 = 5` は `contradiction` では示せない
-#guard_msgs (drop warning) in --#
 #check_failure (by contradiction : 1 + 4 = 5)
diff --git a/LeanByExample/Diagnostic/Synth.lean b/LeanByExample/Diagnostic/Synth.lean
@@ -44,7 +44,6 @@ Additional diagnostic information may be available using the `set_option diagnos
 #guard_msgs in #synth Inv Nat
 
 -- Inv のインスタンスになっていない
-#guard_msgs (drop warning) in --#
 #check_failure (inferInstance : Inv Nat)
 
 /- 自分で無理やり `ℕ` を `Inv` のインスタンスにしてみると、通るようになります。ここでは逆数関数を常に `1` になる定数関数としてみましょう。-/
diff --git a/LeanByExample/Modifier/Local.lean b/LeanByExample/Modifier/Local.lean
@@ -11,12 +11,10 @@ section foo
 end foo
 
 -- section を抜けると使えなくなる
-#guard_msgs (drop warning) in --#
 #check_failure succ'
 
 section foo
   -- 同じ名前の section を再度開いても使えない
-  #guard_msgs (drop warning) in --#
   #check_failure succ'
 end foo
 
@@ -31,13 +29,11 @@ namespace hoge
 end hoge
 
 -- namespace の外では使用できない
-#guard_msgs (drop warning) in --#
 #check_failure succ' 2
 
 -- 再び同じ名前の namespace をオープンする
 namespace hoge
   -- 使用できない！
-  #guard_msgs (drop warning) in --#
   #check_failure succ'
 end hoge
 
@@ -89,7 +85,6 @@ section
 end
 
 -- section を抜けると使えなくなる
-#guard_msgs (drop warning) in --#
 #check_failure (0 : MyNat)
 
 /- ## 属性に対する local
@@ -115,7 +110,6 @@ section
 end
 
 -- section を抜けると simp 補題が利用できなくなる
-#guard_msgs (drop warning) in --#
 #check_failure (by simp : MyNat.add .zero .zero = .zero)
 
 /- ## 構文的な性質
diff --git a/LeanByExample/Modifier/Private.lean b/LeanByExample/Modifier/Private.lean
@@ -18,7 +18,6 @@ import Lean --#
 #check Point.sub
 
 -- private とマークした定義にはアクセスできない
-#guard_msgs (drop warning) in --#
 #check_failure Point.private_sub
 
 /- なお `private` コマンドで定義した名前は、同じファイル内であればそのセクションや名前空間を出ても普通にアクセスすることができます。特に、`private` は [`protected`](#{root}/Modifier/Protected.md) の効果を持ちません。-/
diff --git a/LeanByExample/Modifier/Protected.lean b/LeanByExample/Modifier/Protected.lean
@@ -13,7 +13,6 @@ namespace Point
     { x := p.x - q.x, y := p.y - q.y }
 
   -- 名前空間の中にいても、短い名前ではアクセスできない
-  #guard_msgs (drop warning) in --#
   #check_failure sub
 
   -- フルネームならアクセスできる
@@ -24,7 +23,6 @@ end Point
 open Point
 
 -- 名前空間を開いていても、短い名前でアクセスできない
-#guard_msgs (drop warning) in --#
 #check_failure sub
 
 -- フルネームならアクセスできる
@@ -77,7 +75,6 @@ open BinTree
 
 -- 名前空間を開いているのに、
 -- コンストラクタに短い名前でアクセスできない
-#guard_msgs (drop warning) in --#
 #check_failure node
 #check BinTree.node
 
@@ -100,7 +97,6 @@ open Sample
 #check bar
 
 -- hoge には短い名前でアクセスできない
-#guard_msgs (drop warning) in --#
 #check_failure hoge
 
 end --#
diff --git a/LeanByExample/Modifier/Scoped.lean b/LeanByExample/Modifier/Scoped.lean
@@ -97,7 +97,6 @@ section
   #check (30 add' 12)
 
   -- greet は使えないまま
-  #guard_msgs (drop warning) in --#
   #check_failure greet
 end
 
diff --git a/LeanByExample/Parser/AnonymousConstructor.lean b/LeanByExample/Parser/AnonymousConstructor.lean
@@ -27,11 +27,11 @@ inductive Sample where
 
 -- 「コンストラクタが一つしかない帰納型でなければ使用できない」というエラーになる
 /--
-warning: invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor ⏎
+error: invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor ⏎
   Sample
 -/
 #guard_msgs in
-  #check_failure (⟨"foo", "bar"⟩ : Sample)
+  #check (⟨"foo", "bar"⟩ : Sample)
 
 /- ## 構造体への使用
 [構造体](#{root}/Declarative/Structure.md)は単一コンストラクタしか持たない帰納型なので、構造体に対しても無名コンストラクタ構文が使用できます。-/
diff --git a/LeanByExample/Parser/ImplicitBinder.lean b/LeanByExample/Parser/ImplicitBinder.lean
@@ -20,7 +20,6 @@ def List.subsₑ (α : Type) (xs : List α) : List (List α) :=
 #eval List.subsₑ Nat [1, 2]
 
 -- 型引数を与えないと（当然ながら）エラーになってしまう
-#guard_msgs (drop warning) in --#
 #check_failure List.subs [1, 2]
 
 /- 引数 `α` を暗黙の引数として受け取るように変更すれば、Lean が `α : Type` の内容を推論してくれるようになり、`α` を省略できるようになります。-/
@@ -37,7 +36,6 @@ def List.subsᵢ {α : Type} (xs : List α) : List (List α) :=
 #eval List.subsᵢ [1, 2]
 
 -- 逆に今度は型引数を与えるとエラーになる
-#guard_msgs (drop warning) in --#
 #check_failure List.subsᵢ Nat [1, 2]
 
 /- ## 明示引数モード
diff --git a/LeanByExample/Tactic/Ext.lean b/LeanByExample/Tactic/Ext.lean
@@ -68,9 +68,7 @@ structure Point (α : Type) where
   y : α
 
 -- 最初は存在しない
-#guard_msgs (drop warning) in --#
 #check_failure Point.ext
-#guard_msgs (drop warning) in --#
 #check_failure Point.ext_iff
 
 -- `Point` に `[ext]` 属性を与える
diff --git a/LeanByExample/Tactic/Induction.lean b/LeanByExample/Tactic/Induction.lean
@@ -220,7 +220,7 @@ def bar : Nat → Nat
   | 0 => 0
   | _ => 1
 
-#guard_msgs (drop warning) in --#
+-- 帰納原理が生成されていない
 #check_failure bar.induct
 
 /- ## よくあるエラー
diff --git a/LeanByExample/Tactic/NativeDecide.lean b/LeanByExample/Tactic/NativeDecide.lean
diff --git a/LeanByExample/Type/List.lean b/LeanByExample/Type/List.lean
diff --git a/LeanByExample/TypeClass/CoeDep.lean b/LeanByExample/TypeClass/CoeDep.lean
diff --git a/LeanByExample/TypeClass/CoeFun.lean b/LeanByExample/TypeClass/CoeFun.lean
diff --git a/LeanByExample/TypeClass/CoeSort.lean b/LeanByExample/TypeClass/CoeSort.lean
diff --git a/LeanByExample/TypeClass/GetElem.lean b/LeanByExample/TypeClass/GetElem.lean
diff --git a/LeanByExample/TypeClass/OfNat.lean b/LeanByExample/TypeClass/OfNat.lean
diff --git a/lake-manifest.json b/lake-manifest.json
diff --git a/lean-toolchain b/lean-toolchain
