Very simple type class fails

Stream: new members

[Andre Graubner (安德)]

Hello everyone, I believe this will be a very silly question, but I can't figure out what's going wrong.
I'm trying to play around with groups based on this document.

However, the second type class is giving me trouble:

class has_mul (α : Type) := (mul : α → α → α)

class semigroup (α : Type) extends has_mul α :=
  (mul_assoc : ∀ a b c : α, a *  b * c = a * (b * c))

has_mul seems to work, but semigroup fails (failed to synthesize type class instance). Am I missing something very obvious here? I feel like this might also just be a version issue, since I've had issues like this due to breaking API changes before.
Thanks for your help!

[Johan Commelin]

@Andre Graubner (安德) What do you have at the top of your file?

[Johan Commelin]

Can you make sure that you are not by accident importing part of mathlibs existing hierarchy?

[Johan Commelin]

If you literally wrote the lines as you pasted them, with nothing in between, then * is certainly referring to the existing has_mul.

[Johan Commelin]

Because you didn't set up your own notation.

[Andre Graubner (安德)]

@Johan Commelin thanks for the reply, I'm trying to avoid this by opening a new namespace:

namespace toy_group

class has_mul (α : Type) := (mul : α → α → α)

class semigroup (α : Type) extends has_mul α :=
  (mul_assoc : ∀ a b c : α, a *  b * c = a * (b * c))

end toy_group

Is this enough?

[Johan Commelin]

You will have to teach Lean that * means has_mul.mul.

[Johan Commelin]

I don't know if you can easily overload.

[Johan Commelin]

You might need to start your file with prelude. Which means you'll not be able to use any predefined things...

[Andre Graubner (安德)]

Thanks, that makes sense.

[Eric Wieser]

If you start with prelude then you won't even get =!

[Andre Graubner (安德)]

Alright, I'll have a look :)

[Johan Commelin]

It might be easier to take has_mul for granted, and start building your stuff from semigroup upwards.

[Andre Graubner (安德)]

That solved it, amazing