Zulip Chat Archive

Stream: general

Topic: Using derived type classes


view this post on Zulip Robert Maxton (Oct 31 2020 at 00:06):

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].

view this post on Zulip Adam Topaz (Oct 31 2020 at 00:26):

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

view this post on Zulip Robert Maxton (Oct 31 2020 at 00:30):

#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

view this post on Zulip Adam Topaz (Oct 31 2020 at 00:32):

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

view this post on Zulip Adam Topaz (Oct 31 2020 at 00:33):

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

view this post on Zulip Adam Topaz (Oct 31 2020 at 00:34):

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

view this post on Zulip Robert Maxton (Oct 31 2020 at 00:35):

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


Last updated: May 10 2021 at 18:22 UTC