From 2b42bf8fe765ecadec78eb3cc68bf33eb2873382 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sat, 9 Nov 2024 03:26:27 +0900
Subject: [PATCH] =?UTF-8?q?`#eval`=20=E3=81=AE=E4=BB=95=E6=A7=98=E5=A4=89?=
 =?UTF-8?q?=E6=9B=B4=E3=81=AB=E4=BC=B4=E3=81=86=E3=82=B3=E3=83=BC=E3=83=89?=
 =?UTF-8?q?=E4=BE=8B=E3=81=AE=E6=9B=B4=E6=96=B0?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Reference/Declarative/Deriving.lean | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

diff --git a/LeanByExample/Reference/Declarative/Deriving.lean b/LeanByExample/Reference/Declarative/Deriving.lean
index c0781ab3..fe5d26df 100644
--- a/LeanByExample/Reference/Declarative/Deriving.lean
+++ b/LeanByExample/Reference/Declarative/Deriving.lean
@@ -11,16 +11,13 @@ inductive Color : Type where
   | green
   | blue
 
--- 最初は `Repr` が定義されていないので `eval` できない
+-- 暗黙的に Repr インスタンスを生成しない
+set_option eval.derive.repr false
+
+-- `Repr` が定義されていないので `eval` できない
 /--
-error: expression
-  Color.red
-has type
+error: could not synthesize a 'Repr' or 'ToString' instance for type
   Color
-but instance
-  Lean.Eval Color
-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.Eval` class
 -/
 #guard_msgs in #eval Color.red