From d57a9bbbe355d4fef4d37de21cae640fc404ac3f Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Tue, 6 Aug 2024 20:38:11 +0900
Subject: [PATCH 1/5] =?UTF-8?q?=E3=83=90=E3=83=BC=E3=82=B8=E3=83=A7?=
 =?UTF-8?q?=E3=83=B3=E6=9B=B4=E6=96=B0=20=F0=9F=9A=A7?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Examples/Command/Declarative/Abbrev.lean        |  2 +-
 Examples/Command/Declarative/Opaque.lean        |  2 +-
 Examples/Command/Declarative/Partial.lean       |  6 +++---
 Examples/Command/Declarative/TerminationBy.lean |  6 +++---
 Examples/Command/Diagnostic/GuardMsgs.lean      |  6 +++---
 Examples/Command/Diagnostic/Synth.lean          |  2 +-
 Examples/Command/Diagnostic/Whnf.lean           | 10 ++++------
 Examples/Tactic/Ext.lean                        |  4 ++--
 Examples/Term/TypeClass/ToString.lean           |  4 ++--
 lake-manifest.json                              | 12 ++++++------
 lean-toolchain                                  |  2 +-
 11 files changed, 27 insertions(+), 29 deletions(-)

diff --git a/Examples/Command/Declarative/Abbrev.lean b/Examples/Command/Declarative/Abbrev.lean
index 4a173e59..f29d1ff7 100644
--- a/Examples/Command/Declarative/Abbrev.lean
+++ b/Examples/Command/Declarative/Abbrev.lean
@@ -16,7 +16,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `42` cannot be used in a context where the expected type is
   NaturalNumber
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in #check (42 : NaturalNumber)
 
diff --git a/Examples/Command/Declarative/Opaque.lean b/Examples/Command/Declarative/Opaque.lean
index 0a19bd67..ac425ae7 100644
--- a/Examples/Command/Declarative/Opaque.lean
+++ b/Examples/Command/Declarative/Opaque.lean
@@ -70,7 +70,7 @@ structure Something where
 /--
 error: failed to synthesize
   Inhabited Something
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in opaque something : Something
 
diff --git a/Examples/Command/Declarative/Partial.lean b/Examples/Command/Declarative/Partial.lean
index f709ccd4..df2115e8 100644
--- a/Examples/Command/Declarative/Partial.lean
+++ b/Examples/Command/Declarative/Partial.lean
@@ -15,12 +15,12 @@ namespace WithoutPartial --#
 error: fail to show termination for
   WithoutPartial.M
 with errors
-structural recursion cannot be used:
-
-argument #1 cannot be used for structural recursion
+failed to infer structural recursion:
+Cannot use parameter n:
   failed to eliminate recursive application
     M (n + 11)
 
+
 failed to prove termination, possible solutions:
   - Use `have`-expressions to prove the remaining goals
   - Use `termination_by` to specify a different well-founded relation
diff --git a/Examples/Command/Declarative/TerminationBy.lean b/Examples/Command/Declarative/TerminationBy.lean
index 157fc7a0..b4bda386 100644
--- a/Examples/Command/Declarative/TerminationBy.lean
+++ b/Examples/Command/Declarative/TerminationBy.lean
@@ -7,12 +7,12 @@ namespace TerminationBy --#
 error: fail to show termination for
   TerminationBy.M
 with errors
-structural recursion cannot be used:
-
-argument #1 cannot be used for structural recursion
+failed to infer structural recursion:
+Cannot use parameter n:
   failed to eliminate recursive application
     M (n + 11)
 
+
 failed to prove termination, possible solutions:
   - Use `have`-expressions to prove the remaining goals
   - Use `termination_by` to specify a different well-founded relation
diff --git a/Examples/Command/Diagnostic/GuardMsgs.lean b/Examples/Command/Diagnostic/GuardMsgs.lean
index 38b910ec..a03d6ef5 100644
--- a/Examples/Command/Diagnostic/GuardMsgs.lean
+++ b/Examples/Command/Diagnostic/GuardMsgs.lean
@@ -12,7 +12,7 @@ import Mathlib.Algebra.Group.Defs -- 逆数を使うために必要 --#
 /--
 error: failed to synthesize
   HAdd ℕ String String
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in #eval (2 + "hello" : String)
 
@@ -26,7 +26,7 @@ variable (α : Type)
 /--
 error: failed to synthesize
   Inv α
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in #check (_ : α)⁻¹
 
@@ -35,6 +35,6 @@ use `set_option diagnostics true` to get diagnostic information
 error:
   failed to synthesize
     Inv α
-  use `set_option diagnostics true` to get diagnostic information
+  Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs (whitespace := lax) in #check (_ : α)⁻¹
diff --git a/Examples/Command/Diagnostic/Synth.lean b/Examples/Command/Diagnostic/Synth.lean
index ed4b11d8..67023d77 100644
--- a/Examples/Command/Diagnostic/Synth.lean
+++ b/Examples/Command/Diagnostic/Synth.lean
@@ -38,7 +38,7 @@ use `set_option diagnostics true` to get diagnostic information
 /--
 error: failed to synthesize
   Inv ℕ
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in #synth Inv Nat
 
diff --git a/Examples/Command/Diagnostic/Whnf.lean b/Examples/Command/Diagnostic/Whnf.lean
index 5545e0cd..fc60dd0f 100644
--- a/Examples/Command/Diagnostic/Whnf.lean
+++ b/Examples/Command/Diagnostic/Whnf.lean
@@ -99,11 +99,10 @@ info: {
             ⟨fun x =>
               (Many.rec ⟨fun x => x, PUnit.unit⟩
                     (fun a a_2 a_ih =>
-                      ⟨fun x => Many.more a fun x_1 => (a_ih PUnit.unit).1 x,
-                        ⟨⟨fun a => (a_ih a).1, fun a => (a_ih a).2⟩, PUnit.unit⟩⟩)
+                      ⟨fun x => Many.more a fun x_1 => (a_ih PUnit.unit).1 x, fun a => (a_ih a).1, fun a => (a_ih a).2⟩)
                     (x a)).1
                 ((a_ih PUnit.unit).1 x),
-              ⟨⟨fun a => (a_ih a).1, fun a => (a_ih a).2⟩, PUnit.unit⟩⟩)
+              fun a => (a_ih a).1, fun a => (a_ih a).2⟩)
           x).1
       fun x => Many.more (f x) fun x => Many.none,
   mapConst := fun {α β} x x_1 =>
@@ -112,11 +111,10 @@ info: {
             ⟨fun x =>
               (Many.rec ⟨fun x => x, PUnit.unit⟩
                     (fun a a_2 a_ih =>
-                      ⟨fun x => Many.more a fun x_2 => (a_ih PUnit.unit).1 x,
-                        ⟨⟨fun a => (a_ih a).1, fun a => (a_ih a).2⟩, PUnit.unit⟩⟩)
+                      ⟨fun x => Many.more a fun x_2 => (a_ih PUnit.unit).1 x, fun a => (a_ih a).1, fun a => (a_ih a).2⟩)
                     (x a)).1
                 ((a_ih PUnit.unit).1 x),
-              ⟨⟨fun a => (a_ih a).1, fun a => (a_ih a).2⟩, PUnit.unit⟩⟩)
+              fun a => (a_ih a).1, fun a => (a_ih a).2⟩)
           x_1).1
       fun x_2 => Many.more x fun x => Many.none }
 -/
diff --git a/Examples/Tactic/Ext.lean b/Examples/Tactic/Ext.lean
index 0204574f..8cafe5cb 100644
--- a/Examples/Tactic/Ext.lean
+++ b/Examples/Tactic/Ext.lean
@@ -45,10 +45,10 @@ attribute [ext] Point
 
 -- 自動生成された定理
 -- 各フィールドの値が等しければ、2つの `Point` は等しいという主張
-#check (Point.ext : (x y : Point α) → x.x = y.x → x.y = y.y → x = y)
+#check (Point.ext : ∀{x y : Point α}, x.x = y.x → x.y = y.y → x = y)
 
 -- 自動生成された定理その２
 -- 2つの `Point` の点が等しいことは、各フィールドの値が等しいことと同値
-#check (Point.ext_iff : (x y : Point α) → x = y ↔ x.x = y.x ∧ x.y = y.y)
+#check (Point.ext_iff : ∀{x y : Point α}, x = y ↔ x.x = y.x ∧ x.y = y.y)
 
 end Ext --#
diff --git a/Examples/Term/TypeClass/ToString.lean b/Examples/Term/TypeClass/ToString.lean
index 850e428d..2653ddbc 100644
--- a/Examples/Term/TypeClass/ToString.lean
+++ b/Examples/Term/TypeClass/ToString.lean
@@ -15,7 +15,7 @@ def origin : Point Int := ⟨0, 0⟩
 /--
 error: failed to synthesize
   ToString (Point Int)
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs (error) in #check s!"{origin}"
 
@@ -57,7 +57,7 @@ def david := Person.mk "David" 42
 /--
 error: failed to synthesize
   ToString Person
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs (error) in #check s!"{david}"
 
diff --git a/lake-manifest.json b/lake-manifest.json
index f5f1366e..e0b4590d 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "41bc768e2224d6c75128a877f1d6e198859b3178",
+   "rev": "dc167d260ff7ee9849b436037add06bed15104be",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6058ab8d938c5104eace7d0fb5ac17b21cb067b1",
+   "rev": "ae6ea60e9d8bc2d4b37ff02115854da2e1b710d0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -45,10 +45,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c87908619cccadda23f71262e6898b9893bffa36",
+   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.40",
+   "inputRev": "v0.0.41",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e7e90d90a62e6d12cbb27cbbfc31c094ee4ecc58",
+   "rev": "68cd8ae0f5b996176d1243d94c56e17de570e3bf",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d56e389960165aa122e7c97c098d67e4def09470",
+   "rev": "04b5a7b3455c83115ae0db6ec9b1d217aac91365",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
diff --git a/lean-toolchain b/lean-toolchain
index 7f0ea50a..64981ae5 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.10.0
+leanprover/lean4:v4.11.0-rc1

From a4cccea0b10079829ad3a0c2d2e5c52f91d97865 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Tue, 6 Aug 2024 20:42:13 +0900
Subject: [PATCH 2/5] =?UTF-8?q?guard=5Fmsgs=20=E3=81=AE=E6=96=87=E7=AB=A0?=
 =?UTF-8?q?=E3=82=92=E5=BE=AE=E4=BF=AE=E6=AD=A3?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Examples/Command/Diagnostic/GuardMsgs.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Examples/Command/Diagnostic/GuardMsgs.lean b/Examples/Command/Diagnostic/GuardMsgs.lean
index a03d6ef5..b4ab6343 100644
--- a/Examples/Command/Diagnostic/GuardMsgs.lean
+++ b/Examples/Command/Diagnostic/GuardMsgs.lean
@@ -6,8 +6,7 @@
 import Mathlib.Algebra.Group.Defs -- 逆数を使うために必要 --#
 
 /-- info: 2 -/
-#guard_msgs in
-#eval 2
+#guard_msgs in #eval 2
 
 /--
 error: failed to synthesize
@@ -16,7 +15,7 @@ Additional diagnostic information may be available using the `set_option diagnos
 -/
 #guard_msgs in #eval (2 + "hello" : String)
 
-/-! ## 空白の扱い
+/- ## 空白の違いを無視させるには
 `#guard_msgs` コマンドは空白の数に敏感で、空白の長さによって通ったり通らなかったりします。しかし、`whitespace` という引数に `lax` を指定することにより、この空白に関する制限は緩めることができます。
 -/
 

From 7eaaa032b903ed26abaeb5e40eac34313ebf4470 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Tue, 6 Aug 2024 20:55:03 +0900
Subject: [PATCH 3/5] =?UTF-8?q?=E3=82=A8=E3=83=A9=E3=83=BC=E3=82=92?=
 =?UTF-8?q?=E6=B6=88=E3=81=99?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Examples/Command/Diagnostic/Print.lean |  6 +++---
 Examples/Command/Diagnostic/Synth.lean | 13 ++++++-------
 Examples/Tactic/NativeDecide.lean      |  6 +++---
 Examples/Term/TypeClass/ToString.lean  |  7 +------
 4 files changed, 13 insertions(+), 19 deletions(-)

diff --git a/Examples/Command/Diagnostic/Print.lean b/Examples/Command/Diagnostic/Print.lean
index 9a0a43bb..aeec6f59 100644
--- a/Examples/Command/Diagnostic/Print.lean
+++ b/Examples/Command/Diagnostic/Print.lean
@@ -56,9 +56,9 @@ but is expected to have type
   TSyntax [`ident, `str] : Type
 -/
 #guard_msgs(error) in
-#eval show Lean.Elab.Term.TermElabM Unit from do
-  let a ← `(Nat.succ Nat.zero)
-  let _b ← `(#print $a)
+  #eval! show Lean.Elab.Term.TermElabM Unit from do
+    let a ← `(Nat.succ Nat.zero)
+    let _b ← `(#print $a)
 
 /- 上のコード例は、これを検証するものです。エラーメッセージにあるように `#print` は `ident` または `str` を期待しており、これはそれぞれ単一の識別子と文字列リテラルを意味します。`Nat.succ Nat.zero` は `term` つまり項なのでエラーになります。
 
diff --git a/Examples/Command/Diagnostic/Synth.lean b/Examples/Command/Diagnostic/Synth.lean
index 67023d77..e1ce924d 100644
--- a/Examples/Command/Diagnostic/Synth.lean
+++ b/Examples/Command/Diagnostic/Synth.lean
@@ -20,7 +20,7 @@ variable (α : Type)
 /--
 error: failed to synthesize
   Inv α
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in #check (_ : α)⁻¹
 
@@ -35,12 +35,11 @@ use `set_option diagnostics true` to get diagnostic information
 
 /-! 自然数 `ℕ` に対しては逆数が定義されていないと予想されますが、実際 `Inv` のインスタンスになっていません。-/
 
-/--
-error: failed to synthesize
-  Inv ℕ
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
--/
-#guard_msgs in #synth Inv Nat
+-- エラーになってしまう
+#guard_msgs (drop error) in #synth Inv Nat
+
+-- 実際、Inv のインスタンスになっていない
+#check_failure (inferInstance : Inv Nat)
 
 /-! 自分で無理やり `ℕ` を `Inv` のインスタンスにしてみると、通るようになります。ここでは逆数関数を常に `1` になる定数関数としてみましょう。-/
 
diff --git a/Examples/Tactic/NativeDecide.lean b/Examples/Tactic/NativeDecide.lean
index 11bebec1..c3428bc2 100644
--- a/Examples/Tactic/NativeDecide.lean
+++ b/Examples/Tactic/NativeDecide.lean
@@ -2,7 +2,7 @@
 # native_decide
 `native_decide` は、式を評価したときに判ることを示すことができます。
 
-たとえば、Lean では再帰関数 `f` を定義したらそれが停止することの証明を求められますが、それを `sorry` で回避したとしましょう。このとき `f` の具体的な値を `#eval` で評価することは依然として可能ですが、その値をとることを `rfl` で証明することはできなくなります。
+たとえば、Lean では再帰関数 `f` を定義したらそれが停止することの証明を求められますが、それを `sorry` で回避したとしましょう。このとき `f` の具体的な値を評価することは `#eval!` を使えば可能ですが、その値をとることを `rfl` で証明することはできなくなります。
 
 しかし、`native_decide` を使うと証明が可能です。
 -/
@@ -18,8 +18,8 @@ def gcd (m n : Nat) : Nat :=
   -- 停止性を証明しない
   decreasing_by sorry
 
--- eval はできる
-#eval gcd 42998431 120019
+-- 値を評価することはできる
+#eval! gcd 42998431 120019
 
 -- `rfl` では証明できない
 -- これは停止性を証明していないため
diff --git a/Examples/Term/TypeClass/ToString.lean b/Examples/Term/TypeClass/ToString.lean
index 2653ddbc..eb4a84d2 100644
--- a/Examples/Term/TypeClass/ToString.lean
+++ b/Examples/Term/TypeClass/ToString.lean
@@ -54,11 +54,6 @@ def david := Person.mk "David" 42
 #eval david
 
 -- `ToString` のインスタンスがないのでエラーになる
-/--
-error: failed to synthesize
-  ToString Person
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
--/
-#guard_msgs (error) in #check s!"{david}"
+#guard_msgs (drop error) in #check s!"{david}"
 
 end ToString --#

From 3eeba5a5b5aace36347cbf5147d2b02ee7d5ba0e Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Tue, 6 Aug 2024 21:10:05 +0900
Subject: [PATCH 4/5] =?UTF-8?q?#guard=5Fmsgs=20=E9=96=A2=E9=80=A3=E3=81=AE?=
 =?UTF-8?q?=E3=83=95=E3=82=A9=E3=83=BC=E3=83=9E=E3=83=83=E3=83=88?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Examples/Command/Declarative/Class.lean    | 10 ++++------
 Examples/Command/Declarative/Infix.lean    |  2 +-
 Examples/Command/Declarative/Local.lean    |  2 +-
 Examples/Command/Declarative/Macro.lean    |  3 ++-
 Examples/Command/Declarative/Notation.lean | 13 -------------
 Examples/Command/Declarative/Partial.lean  | 12 ++++++------
 Examples/Command/Declarative/Scoped.lean   |  2 +-
 Examples/Tactic/AcRfl.lean                 | 15 +++++----------
 Examples/Tactic/Dsimp.lean                 |  2 +-
 9 files changed, 21 insertions(+), 40 deletions(-)

diff --git a/Examples/Command/Declarative/Class.lean b/Examples/Command/Declarative/Class.lean
index f1ecacc9..acbfd7fb 100644
--- a/Examples/Command/Declarative/Class.lean
+++ b/Examples/Command/Declarative/Class.lean
@@ -57,8 +57,7 @@ def instMonoid'Nat : Monoid' Nat where
 
 /- このとき構造体 `Monoid'` のフィールド `Monoid'.e` は、「`Monoid'` の項に対して `α` の要素を返す」関数なので、次のような型を持ちます。-/
 
-/-- info: Class.Monoid'.e {α : Type} (self : Monoid' α) : α -/
-#guard_msgs in #check Monoid'.e
+#check (Monoid'.e : {α : Type} → (self : Monoid' α) → α)
 
 /- `self : Monoid' α` が暗黙の引数ではなく明示的な引数なので、型クラスのように書くことはできません。-/
 
@@ -72,8 +71,7 @@ def instMonoid'Nat : Monoid' Nat where
 
 ここで(本物の)型クラスにおける単位元関数 `e` の型を調べてみると、`self : Monoid' α` が角括弧 `[ .. ]` で囲われていることがわかります。-/
 
-/-- info: Class.Monoid.e {α : Type} [self : Monoid α] : α -/
-#guard_msgs in #check Monoid.e
+#check (Monoid.e : {α : Type} → [self : Monoid α] → α)
 
 /- これは**インスタンス暗黙引数**と呼ばれるもので、この場合 Lean に対して `Monoid' α` 型の項を自動的に合成するよう指示することを意味します。また、型クラスのインスタンス暗黙引数を自動的に合成する手続きのことを、**型クラス解決**と呼びます。-/
 
@@ -178,6 +176,7 @@ instance : HasCardinal Bool := by
 inductive Ordinal : Type where
   | nat (n : Nat) : Ordinal
   | omega : Ordinal
+deriving DecidableEq
 
 def Ordinal.toString : Ordinal → String
   | Ordinal.nat n => ToString.toString n
@@ -195,7 +194,6 @@ def HasCardinal.card (X : Type) [h : HasCardinal X] : Ordinal :=
 export HasCardinal (card)
 
 -- Bool の濃度が計算できた
-/-- info: 2 -/
-#guard_msgs in #eval card Bool
+#guard card Bool = Ordinal.nat 2
 
 end Class --#
diff --git a/Examples/Command/Declarative/Infix.lean b/Examples/Command/Declarative/Infix.lean
index f0f4e9c4..9f539787 100644
--- a/Examples/Command/Declarative/Infix.lean
+++ b/Examples/Command/Declarative/Infix.lean
@@ -59,6 +59,6 @@ elab "#expand_command " t:command : command => do
 
 /-- info: notation:50 lhs✝:51 " LXOR " rhs✝:51 => lxor lhs✝ rhs✝ -/
 #guard_msgs in
-#expand_command infix:50 " LXOR " => lxor
+  #expand_command infix:50 " LXOR " => lxor
 
 end Infix --#
diff --git a/Examples/Command/Declarative/Local.lean b/Examples/Command/Declarative/Local.lean
index 33e17420..b8ca5cdb 100644
--- a/Examples/Command/Declarative/Local.lean
+++ b/Examples/Command/Declarative/Local.lean
@@ -65,7 +65,7 @@ error: <input>:1:6: expected 'binder_predicate', 'builtin_dsimproc', 'builtin_si
 'notation', 'postfix', 'prefix', 'simproc', 'syntax' or 'unif_hint'
 -/
 #guard_msgs in
-run_meta checkParse `command "local def"
+  run_meta checkParse `command "local def"
 
 /-
 数が多いためすべての例を挙げることはしませんが、いくつか紹介します。たとえば `instance` の場合、`local` を付けて登録したインスタンスがその `section` の内部限定になります。
diff --git a/Examples/Command/Declarative/Macro.lean b/Examples/Command/Declarative/Macro.lean
index c4d78434..4636e77b 100644
--- a/Examples/Command/Declarative/Macro.lean
+++ b/Examples/Command/Declarative/Macro.lean
@@ -15,7 +15,8 @@ def checkParse (cat : Name) (s : String) : MetaM Unit := do
 
 -- 最初は `#greet` が未定義なので、合法的なLeanのコマンドとして認識されない
 /-- error: <input>:1:0: expected command -/
-#guard_msgs in run_meta checkParse `command "#greet"
+#guard_msgs in
+  run_meta checkParse `command "#greet"
 
 -- `#greet` コマンドを定義する
 scoped macro "#greet " : command => `(#eval "Hello World!")
diff --git a/Examples/Command/Declarative/Notation.lean b/Examples/Command/Declarative/Notation.lean
index 3e584454..3809e893 100644
--- a/Examples/Command/Declarative/Notation.lean
+++ b/Examples/Command/Declarative/Notation.lean
@@ -130,19 +130,6 @@ set_option pp.mvars false
 
 -- 等号（優先順位 50）より優先順位が低いという問題でエラーになる
 -- 上では60で定義しているのに、なぜ？
-/--
-warning: application type mismatch
-  Sum true
-argument
-  true
-has type
-  Bool : Type
-but is expected to have type
-  Type _ : Type (_ + 1)
----
-info: sorryAx (Type u_1) true ⊕ sorryAx (Type u_2) true : Type (max u_1 u_2)
--/
-#guard_msgs in
 #check_failure true ⊕ true = false
 
 -- 括弧を付けるとエラーにならない
diff --git a/Examples/Command/Declarative/Partial.lean b/Examples/Command/Declarative/Partial.lean
index df2115e8..d48b8627 100644
--- a/Examples/Command/Declarative/Partial.lean
+++ b/Examples/Command/Declarative/Partial.lean
@@ -30,12 +30,12 @@ h✝ : ¬n > 100
 ⊢ n + 11 < n
 -/
 #guard_msgs in
-/-- McCarthy の 91 関数 -/
-def M (n : Nat) : Nat :=
-  if n > 100 then
-    n - 10
-  else
-    M (M (n + 11))
+  /-- McCarthy の 91 関数 -/
+  def M (n : Nat) : Nat :=
+    if n > 100 then
+      n - 10
+    else
+      M (M (n + 11))
 
 end WithoutPartial --#
 namespace Partial --#
diff --git a/Examples/Command/Declarative/Scoped.lean b/Examples/Command/Declarative/Scoped.lean
index 3893a546..103279fb 100644
--- a/Examples/Command/Declarative/Scoped.lean
+++ b/Examples/Command/Declarative/Scoped.lean
@@ -62,7 +62,7 @@ error: <input>:1:7: expected 'binder_predicate', 'builtin_dsimproc', 'builtin_si
 'syntax' or 'unif_hint'
 -/
 #guard_msgs in
-run_meta checkParse `command "scoped def"
+  run_meta checkParse `command "scoped def"
 
 /- ## open scoped
 `open scoped` コマンドを利用すると、特定の名前空間にある `scoped` が付けられた名前だけを有効にすることができます。単に [`open`](./Open.md) コマンドを利用するとその名前空間にあるすべての名前が有効になります。
diff --git a/Examples/Tactic/AcRfl.lean b/Examples/Tactic/AcRfl.lean
index eb78ecfd..ce8bb9f1 100644
--- a/Examples/Tactic/AcRfl.lean
+++ b/Examples/Tactic/AcRfl.lean
@@ -87,16 +87,11 @@ local に宣言したので、このセクション内限定 -/
 local instance : Std.Commutative (α := Color) (· + ·) where
   comm := Color.add_comm
 
-/--
-error: tactic 'rfl' failed, equality lhs
-  a + b
-is not definitionally equal to rhs
-  b + a
-a b : Color
-⊢ a + b = b + a
--/
-#guard_msgs in example (a b : Color) : a + b = b + a := by
-  ac_rfl
+example (a b : Color) : a + b = b + a := by
+  -- ac_rfl がエラーになってしまう
+  fail_if_success ac_rfl
+
+  ext <;> apply Nat.add_comm
 
 end
 /- ## 結合法則と ac_rfl
diff --git a/Examples/Tactic/Dsimp.lean b/Examples/Tactic/Dsimp.lean
index 2d5a3fc3..37f2f515 100644
--- a/Examples/Tactic/Dsimp.lean
+++ b/Examples/Tactic/Dsimp.lean
@@ -162,4 +162,4 @@ run_meta checkParse `tactic "unfold Inter.inter"
 -- 識別子でないものを渡すとパースできない
 /-- error: <input>:1:7: expected identifier -/
 #guard_msgs in
-run_meta checkParse `tactic "unfold (· ∩ ·)"
+  run_meta checkParse `tactic "unfold (· ∩ ·)"

From ef7346171c8baae250eb001dd621f6ed18224e03 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Tue, 6 Aug 2024 21:15:56 +0900
Subject: [PATCH 5/5] =?UTF-8?q?`#guard=5Fmsgs=20(drop=20error)`=20?=
 =?UTF-8?q?=E3=81=AF=E3=82=A8=E3=83=A9=E3=83=BC=E3=81=8C=E3=81=AA=E3=81=8F?=
 =?UTF-8?q?=E3=81=A6=E3=82=82=E6=88=90=E5=8A=9F=E3=81=99=E3=82=8B=E3=81=AE?=
 =?UTF-8?q?=E3=81=A7=E4=BD=BF=E7=94=A8=E3=81=97=E3=81=AA=E3=81=84?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Examples/Command/Diagnostic/Eval.lean  | 22 ++++++++++++++++++++--
 Examples/Command/Diagnostic/Synth.lean |  9 +++++++--
 Examples/Tactic/AcRfl.lean             |  9 +++++++--
 Examples/Term/TypeClass/ToString.lean  |  9 ++++++++-
 4 files changed, 42 insertions(+), 7 deletions(-)

diff --git a/Examples/Command/Diagnostic/Eval.lean b/Examples/Command/Diagnostic/Eval.lean
index cbe76893..a21ff35f 100644
--- a/Examples/Command/Diagnostic/Eval.lean
+++ b/Examples/Command/Diagnostic/Eval.lean
@@ -26,10 +26,28 @@ def main : IO Unit :=
 式の評価を行うコマンドであるため、型や関数など、評価のしようがないものを与えるとエラーになります。-/
 
 -- 型は評価できない
-#guard_msgs (drop error) in #eval Nat
+/--
+error: expression
+  ℕ
+has type
+  Type
+but instance
+  Lean.MetaEval Type
+failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class
+-/
+#guard_msgs in #eval Nat
 
 -- 関数そのものも評価できない
-#guard_msgs (drop error) in #eval (fun x => x + 1)
+/--
+error: expression
+  fun x => x + 1
+has type
+  ℕ → ℕ
+but instance
+  Lean.MetaEval (ℕ → ℕ)
+failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class
+-/
+#guard_msgs in #eval (fun x => x + 1)
 
 /- 一般に、[`Repr`](../../Term/TypeClass/Repr.md) や [`ToString`](../../Term/TypeClass/ToString.md) のインスタンスでないような型の項は `#eval` に渡すことができません。-/
 
diff --git a/Examples/Command/Diagnostic/Synth.lean b/Examples/Command/Diagnostic/Synth.lean
index e1ce924d..e6e751ae 100644
--- a/Examples/Command/Diagnostic/Synth.lean
+++ b/Examples/Command/Diagnostic/Synth.lean
@@ -36,9 +36,14 @@ Additional diagnostic information may be available using the `set_option diagnos
 /-! 自然数 `ℕ` に対しては逆数が定義されていないと予想されますが、実際 `Inv` のインスタンスになっていません。-/
 
 -- エラーになってしまう
-#guard_msgs (drop error) in #synth Inv Nat
+/--
+error: failed to synthesize
+  Inv ℕ
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
+-/
+#guard_msgs in #synth Inv Nat
 
--- 実際、Inv のインスタンスになっていない
+-- Inv のインスタンスになっていない
 #check_failure (inferInstance : Inv Nat)
 
 /-! 自分で無理やり `ℕ` を `Inv` のインスタンスにしてみると、通るようになります。ここでは逆数関数を常に `1` になる定数関数としてみましょう。-/
diff --git a/Examples/Tactic/AcRfl.lean b/Examples/Tactic/AcRfl.lean
index ce8bb9f1..2fb704b2 100644
--- a/Examples/Tactic/AcRfl.lean
+++ b/Examples/Tactic/AcRfl.lean
@@ -105,8 +105,13 @@ protected theorem add_assoc (a b c : Color) : a + b + c = a + (b + c) := by
 
 -- エラーになっているので、
 -- Commutative のインスタンスはないことが確認できる
-#guard_msgs (drop error) in
-#synth Std.Commutative (α := Color) (· + ·)
+/--
+error: failed to synthesize
+  Std.Commutative fun x x_1 => x + x_1
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
+-/
+#guard_msgs in
+  #synth Std.Commutative (α := Color) (· + ·)
 
 /-- `add_comm` を `Std.Associative` に登録する。
 local にしたのでセクション内でのみ有効 -/
diff --git a/Examples/Term/TypeClass/ToString.lean b/Examples/Term/TypeClass/ToString.lean
index eb4a84d2..eba719b7 100644
--- a/Examples/Term/TypeClass/ToString.lean
+++ b/Examples/Term/TypeClass/ToString.lean
@@ -54,6 +54,13 @@ def david := Person.mk "David" 42
 #eval david
 
 -- `ToString` のインスタンスがないのでエラーになる
-#guard_msgs (drop error) in #check s!"{david}"
+/--
+error: failed to synthesize
+  ToString Person
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
+---
+info: toString "" ++ sorryAx String true ++ toString "" : String
+-/
+#guard_msgs in #check s!"{david}"
 
 end ToString --#