From f9aa505670e44d8788e628ecfd4f3baf999a0d1e Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Fri, 10 Jan 2025 02:27:28 +0900
Subject: [PATCH] =?UTF-8?q?`[coe]`=20=E3=81=A8=20`norm=5Fcast`=20=E3=81=A8?=
 =?UTF-8?q?=E3=81=AE=E9=96=A2=E4=BF=82=E3=82=92=E6=98=8E=E8=A8=98=E3=81=99?=
 =?UTF-8?q?=E3=82=8B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Attribute/Coe.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/LeanByExample/Attribute/Coe.lean b/LeanByExample/Attribute/Coe.lean
index fa9ba165..4433497d 100644
--- a/LeanByExample/Attribute/Coe.lean
+++ b/LeanByExample/Attribute/Coe.lean
@@ -1,7 +1,6 @@
 /- # coe
 
-`[coe]` 属性は、特定の関数を型強制を行う関数として登録し、`↑` 記号で表示されるようにします。
--/
+`[coe]` 属性は、特定の関数を型強制を行う関数として登録し、`↑` 記号で表示されるようにします。-/
 
 /-- 自前で定義した自然数 -/
 inductive MyNat where
@@ -16,6 +15,8 @@ attribute [coe] MyNat.succ
 #guard_msgs in
   #check (MyNat.succ .zero : MyNat)
 
+/- また、`[coe]` 属性は [`norm_cast`](#{root}/Tactic/NormCast.md) タクティクとも関係があります。-/
+
 /- ## 用途
 型強制を [`Coe`](../TypeClass/Coe.md) 型クラスで登録しただけでは、必ずしも型強制を行う関数が `↑` 記号で表示されるわけではありません。`[coe]` 属性を付与することにより、より「型強制らしく」表示されるようになります。
 -/