Using derived type classes

Stream: general

[Robert Maxton]

I think I'm misunderstanding something about derived/extended type classes. I'd like to work with finite groups, so I thought I'd define

class fin_group (G: Type*) extends group G, fintype G

but functions that, for example, rely on [fintype G] don't seem to be satisfied by providing a [fin_group G].

[Adam Topaz]

Can you give a #mwe with something that doesn't work?

[Robert Maxton]

#check λ (G: Type*) [fin_group G], fintype.card G

throws

failed to synthesize type class instance for
G : Type ?,
_inst_1 : fin_group G
⊢ fintype G

[Adam Topaz]

import algebra
import data.fintype.basic

class fin_group (G: Type*) extends group G, fintype G

variables (G : Type*) [fin_group G]
#check fintype.card G

[Adam Topaz]

What you wrote doesn't work because lean can't put the fin_group instance in the typeclass system when its under a lambda.

[Adam Topaz]

This is a hack that gets around this issue:

import algebra
import data.fintype.basic

class fin_group (G: Type*) extends group G, fintype G

#check λ (G : Type*) (I : fin_group G), by exactI fintype.card G

[Robert Maxton]

Hm. That's interesting. I'll play around with that, thanks.