[coe] と norm_cast との関係を明記する

lean-ja · Jan 9, 2025 · f9aa505 · f9aa505
1 parent 32fc81d
commit f9aa505
Showing 1 changed file with 3 additions and 2 deletions.
diff --git 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]` 属性を付与することにより、より「型強制らしく」表示されるようになります。
 -/