From f749dc9d1b1d7e8ab4e5ff55e886757f6fcf6c8a Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Tue, 10 Dec 2024 00:26:04 +0900
Subject: [PATCH] =?UTF-8?q?`abbrev`=20=E3=81=AF=20`@[reducible]=20def`=20?=
 =?UTF-8?q?=E3=81=A8=E5=90=8C=E3=81=98=E3=81=A8=E3=81=84=E3=81=86=E4=B8=BB?=
 =?UTF-8?q?=E5=BC=B5=E3=81=AF=E6=A0=B9=E6=8B=A0=E3=81=8C=E3=81=AA=E3=81=84?=
 =?UTF-8?q?=20Fixes=20#1197?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Reference/Declarative/Abbrev.lean | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/LeanByExample/Reference/Declarative/Abbrev.lean b/LeanByExample/Reference/Declarative/Abbrev.lean
index ddd18c33..349235d2 100644
--- a/LeanByExample/Reference/Declarative/Abbrev.lean
+++ b/LeanByExample/Reference/Declarative/Abbrev.lean
@@ -30,11 +30,13 @@ abbrev NaturalNumber : Type := Nat
 
 end Abbrev1 --#
 /- ## 舞台裏
-`abbrev` は `[reducible]` 属性のついた `def` と同じであり、定義に `[reducible]` 属性を与えても同様のことができます。-/
-namespace Abbrev2 --#
+`abbrev` コマンドを使用すると、裏で `[reducible]` 属性が付与されます。-/
 
-@[reducible] def NaturalNumber : Type := Nat
-
-#check (42 : NaturalNumber)
+abbrev NaturalNumber : Type := Nat
 
-end Abbrev2 --#
+-- `[reducible]` 属性が付与されている
+/--
+info: @[reducible] def NaturalNumber : Type :=
+Nat
+-/
+#guard_msgs in #print NaturalNumber