Zulip Chat Archive
Stream: new members
Topic: difference between `default_instance` and instance`priority`
Asei Inoue (Sep 22 2024 at 16:45):
class Diamond (α : Type) where
dia : α
notation "⋄" => Diamond.dia
section
local instance instDiaZero : Diamond Nat where
dia := 0
local instance instDiaOne : Diamond Nat where
dia := 1
-- there are two instances
-- but latter is used
#guard (⋄ : Nat) = 1
attribute [default_instance] instDiaZero
-- [default_instance] attribute does nothing
#guard (⋄ : Nat) = 1
end
section
local instance (priority := high) instDiaZero' : Diamond Nat where
dia := 0
local instance instDiaOne' : Diamond Nat where
dia := 1
-- priority works
#guard (⋄ : Nat) = 0
end
Asei Inoue (Sep 22 2024 at 16:46):
I do not understand why this behaviour occurs. Please tell me what is the difference between giving the [default_instance]
attribute and setting the priority of the instance high.
Kyle Miller (Sep 22 2024 at 17:58):
default_instance
is orthogonal to priority. Priority adjusts the order in which instances are considered. When all instance problems are stuck, then Lean looks for a default_instance
that can apply.
Default instances are how number literals eventually become Nat
literals if there is no other type information.
Kyle Miller (Sep 22 2024 at 18:00):
If I remember correctly, the algorithm is
Start:
try to synthesize all instance problems
catch stuck instance problems error
for each stuck problem
if there is a default instance that applies
apply it
goto Start
throw the stuck instance problems error
Asei Inoue (Sep 23 2024 at 02:05):
@Kyle Miller Thank you. no.[default_instance]
is for OfNat
only?
Last updated: May 02 2025 at 03:31 UTC