abbrev: reducible な def と同じであると明記する

Src/Abbrev.lean

@@ -8,9 +8,14 @@ namespace Abbrev0 --#
 
 def NaturalNumber : Type := Nat
 
-/- しかし，ここで定義した `Nat` の別名を項に対して使用するとエラーになります． [^fplean] -/
+/- しかし，ここで定義した `Nat` の別名を項に対して使用するとエラーになります．これは，Lean が `NaturalNumber` を定義に簡約(reduce)するよりも先に，`42 : NaturalNumber` という表記が定義されているか `OfNat` のインスタンスを探そうとするためです．-/
 
-#check_failure (42 : NaturalNumber)
+/--
+error: failed to synthesize instance
+  OfNat NaturalNumber 42
+-/
+#guard_msgs in --#
+#check (42 : NaturalNumber)
 
 end Abbrev0 --#
 /- ここでエラーを修正する方法の一つが，`def` の代わりに `abbrev` を使用することです．-/
@@ -21,9 +26,8 @@ abbrev NaturalNumber : Type := Nat
 #check (42 : NaturalNumber)
 
 end Abbrev1 --#
-/- ## reducible 属性
-
-あるいは，定義に `reducible` という属性を与えても機能します． -/
+/- ## 舞台裏
+`abbrev` は `@[reducible]` 属性のついた `def` と同じであるため，定義に `reducible` という属性を与えても機能します． -/
 namespace Abbrev2 --#
 
 @[reducible]
@@ -32,4 +36,3 @@ def NaturalNumber : Type := Nat
 #check (42 : NaturalNumber)
 
 end Abbrev2 --#
-/- [^fplean]: 詳細については [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/getting-to-know/functions-and-definitions.html#messages-you-may-meet) を参照のこと．-/