typeclass inference is not unfolding `def`

Stream: new members

[attoknot]

Hi. I want to play around with the groups, but

def G := Perm (Fin 5)
def GG : Group G := Perm.permGroup  -- this doesn't help

def a : G := c[1,2]
def b : G := c[3,4]

#check MulAction.orbitRel G G  -- failed to synthesize `Group G`
#check MulAction.orbitRel (Perm (Fin 5)) (Perm (Fin 5))  -- works

[Aaron Liu]

This is behavior is intended. You can make you definitions transparent to typeclass by using abbrev or @[reducible] def instead of def.

[attoknot]

thank you for a quick solution!

[Aaron Liu]

you should also consider not using a definition at all and instead defining notation for your groups.