How to define a field of a structure to have type class

Stream: new members

[Rui Liu]

Can I somehow define a field of a structure to have particular type class(es)?

[Alex J. Best]

Can you give an example of what you want? I'm not sure what you mean

[Rui Liu]

Here's an example:

structure T :=
    mk :: (a: Type) (b : a)

def f {t: T}: bool := ite (t.b = t.b) tt ff

This code fails to compile and we need to explicitly decorate with type class decidable_eq.

structure T :=
    mk :: (a: Type) (b : a)

def f {t: T} [h: decidable_eq t.a]: bool := ite (t.b = t.b) tt ff

This is a lot of boilerplate if you have a lot of functions and you need to decorate all of them. What I want is something like this that decorates the field a as a type with decidable_eq class globally:

structure T :=
    mk :: (a: Type) [h: decidable_eq a] (b : a)

def f {t: T} : bool := ite (t.b = t.b) tt ff

However this doesn't compile, so what's the correct way to do it?

[Kevin Buzzard]

Add the missing instance after the definition of the structure

[Kevin Buzzard]

Unrelated -- it's hard to imagine the unifier ever being able to figure out t -- maybe round brackets would be better

[Rui Liu]

That works!

[Eric Wieser]

Shorter to write attribute [instance] T.h, which I think also works