class instance inside a struct?

Stream: new members

[Yannick Seurin]

Is it possible to have a class instance inside a structure? E.g., something like:

import Mathlib

structure Foo where
  α : Type
  deq : DecidableEq α

variable {foo : Foo}

def bar [DecidableEq foo.α] (a b : foo.α) : ℕ :=
  if a = b then 1 else 0 -- works

def bar' (a b : foo.α) : ℕ :=
  if a = b then 1 else 0
-- failed to synthesize Decidable (a = b)

Why can't the class inference system find foo.deq when defining bar', and what would be the correct way to do this?

[Kenny Lau]

import Mathlib

structure Foo where
  α : Type
  deq : DecidableEq α
attribute [instance] Foo.deq

variable {foo : Foo}

def bar (a b : foo.α) : ℕ :=
  if a = b then 1 else 0

you need to explicitly instruct Lean to register the instance using attribute [instance] Foo.deq

[Kenny Lau]

just because it's "there" doesn't mean Lean will automatically use it

[Kenny Lau]

but I believe there has been discussions about possibly changing this by allowing attributes in a structure

[Yannick Seurin]

Great, thanks! ChatGPT gave me 5 different answers (3 of which were wrong), but not this one :sweat_smile:

[Robin Arnez]

It's often a good idea to make the field instance implicit as well, i.e.

structure Foo where
  α : Type
  [deq : DecidableEq α]
attribute [instance] Foo.deq

That way, you can omit the instance when constructing values of type Foo:

structure Foo where
  α : Type
  [deq : DecidableEq α]
attribute [instance] Foo.deq

example : Foo where
  α := Nat