#guard_msgs (drop error) はエラーがなくても成功するので使用しない

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` に渡すことができません。-/
 

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` になる定数関数としてみましょう。-/

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 にしたのでセクション内でのみ有効 -/

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 --#