[default_instance] 属性を紹介する

[Seasawher]

使用例は、OfNat インスタンスをNatではなくて他の集合に移すなど。

def NatPair := Nat × Nat

instance instNatPair : OfNat NatPair 0 := ⟨(0, 0)⟩

/-- info: 0 : Nat -/
#guard_msgs in #check 0

attribute [default_instance] instNatPair

/-- info: 0 : NatPair -/
#guard_msgs in #check 0

TPiLにも例があった気がする

[Seasawher]

TPiL における [default_instance] の使用例

namespace Hidden

class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  hMul : α → β → γ

export HMul (hMul)

instance instHMulInt : HMul Int Int Int where
  hMul := Int.mul

-- Error "typeclass instance problem is stuck, it is often due to metavariables HMul ?m.89 ?m.90 ?m.91"
-- `y` の型を明示的に与えればエラーは消える
#check_failure fun y => (fun x => x * y)

attribute [default_instance] instHMulInt

#check fun y => (fun x => x * y)

end Hidden

[Seasawher]

Zulip: >
difference between default_instance and instancepriority