Merge pull request #1198 from lean-ja/Seasawher/issue1197

`abbrev` は `@[reducible] def` と同じという主張は根拠がない
lean-ja · Dec 9, 2024 · ca179f4 · ca179f4
2 parents e4f56c0 + f749dc9
commit ca179f4
Showing 1 changed file with 8 additions and 6 deletions.
diff --git 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