## Stream: new members

### Topic: How to define a field of a structure to have type class

#### Rui Liu (Dec 13 2020 at 01:09):

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

#### Alex J. Best (Dec 13 2020 at 02:09):

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

#### Rui Liu (Dec 13 2020 at 12:54):

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 (Dec 13 2020 at 15:02):

Add the missing instance after the definition of the structure

#### Kevin Buzzard (Dec 13 2020 at 15:03):

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

That works!

#### Eric Wieser (Dec 13 2020 at 20:58):

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

Last updated: May 13 2021 at 17:42 UTC