Typeclasses in structures

Stream: lean4

[Bolton Bailey]

Suppose I want to include a type with a typeclass in a structure like this, and then later use that typeclass

import Mathlib.Algebra.Field.Basic

structure FooBar where
  MyType : Type

  MyFirstTypeFintype : Field MyFirstType

  val1 : MyType
  val2 : MyType


def FooBar.baz (x : FooBar) : Prop :=
    x.val1 * 2 = x.val2 -- failed to synthesize HMul

Is there a way to let the function know to use the typeclass from the struct without passing it in to the function?

[Henrik Böving]

class Foo (a : Type) where
  default : a

structure Box where
  (a : Type)
  [inst : Foo a]

attribute [instance] Box.inst

def func (b : Box) : b.a := Foo.default

[Henrik Böving]

The [] in the structure declaration makes it such that the argument to the constructor of Box is figured out by the typeclass system, the instance attribute makes the type class search aware of it.

[Bolton Bailey]

I had tried the square brackets and got excited when it wasn't a syntax error, but I was confused when that alone didn't work. Thanks @Henrik Böving!

[Henrik Böving]

Hmm, I'm wondering, is there a good reason that the brackets don't imply the instance attribute automatically?

[Henrik Böving]

If there isn't this just seems like a little UX quirk that we might want to stop happening?