default_instance のページの校正

lean-ja · Jan 12, 2025 · 5c1cb06 · 5c1cb06
1 parent 4804f3f
commit 5c1cb06
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/LeanByExample/Attribute/DefaultInstance.lean b/LeanByExample/Attribute/DefaultInstance.lean
@@ -25,7 +25,7 @@ attribute [default_instance] Int.instMul
 #reduce fun y => (fun x => x * y)
 
 /- ## 用途
-典型的な使用方法は、[`OfNat`](../TypeClass/OfNat.md) 型クラスの（型を指定しない場合の）解釈のされ方を変更することでしょう。
+典型的な使用方法は、[`OfNat`](#{root}/TypeClass/OfNat.md) 型クラスの（型を指定しない場合の）解釈のされ方を変更することでしょう。
 -/
 
 /-- 自然数の対 -/
@@ -52,7 +52,7 @@ attribute [default_instance] instNatPair
 
 /- ## インスタンス優先度との違い
 
-インスタンス優先度(priority)という機能もあります。これも型クラス解決の優先度に関係する機能ですが、`[default_instance]` 属性とは挙動が異なります。Lean はインスタンス解決の際にまずインスタンス優先度の高いものから試し、すべて失敗した場合にのみ `[default_instance]` 属性を参照します。つまり、考慮される順番が異なるということです。
+**インスタンス優先度(priority)** という機能もあります。これも型クラス解決の優先度に関係する機能ですが、`[default_instance]` 属性とは挙動が異なります。Lean はインスタンス解決の際にまずインスタンス優先度の高いものから試し、すべて失敗した場合にのみ `[default_instance]` 属性を参照します。つまり、考慮される順番が異なるということです。
 -/
 
 /-- ⋄ 記法のための型クラス -/