From 5c1cb0612bec726337e93aff6775916785135e1d Mon Sep 17 00:00:00 2001 From: Seasawher Date: Mon, 13 Jan 2025 03:33:16 +0900 Subject: [PATCH] =?UTF-8?q?default=5Finstance=20=E3=81=AE=E3=83=9A?= =?UTF-8?q?=E3=83=BC=E3=82=B8=E3=81=AE=E6=A0=A1=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Attribute/DefaultInstance.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/LeanByExample/Attribute/DefaultInstance.lean b/LeanByExample/Attribute/DefaultInstance.lean index 6437604e..3b99fd94 100644 --- 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]` 属性を参照します。つまり、考慮される順番が異なるということです。 -/ /-- ⋄ 記法のための型クラス -/