Monoid instance confusing syntax error

Stream: lean4

[James Sully]

Hi, I'm trying to write a monoid instance, like so:

structure Round where
  blue : Nat
  green : Nat
  red : Nat

instance : Monoid Round where
  unit := { blue := 0, green := 0, red := 0 }
  op (r1 r2 : Round) := { blue := r1.blue + r2.blue, green := r1.green + r2.green, red := r1.red + r2.red }

I'm getting the error:

▶ 12:12-12:24: error:
function expected at
  Monoid
term has type
  ?m.445

I can't understand why a function is expected. What have I done wrong?

[Yaël Dillies]

You forgot to import docs#Monoid !

[Yaël Dillies]

set_option autoImplicit false and you will get the sensible error message instead of the obscure one.

[James Sully]

Ah, I assumed it would be in the prelude or whatever.
is it
import Mathlib.Algebra.Group.Defs? I get unknown package Mathlib, I guess I have to depend on it somehow?

[James Sully]

Yaël Dillies said:

set_option autoImplicit false and you will get the sensible error message instead of the obscure one.

does this just go in the source?

[Yaël Dillies]

Yes

set_option autoImplicit false

instance : Monoid Round where
  unit := { blue := 0, green := 0, red := 0 }
  op (r1 r2 : Round) := { blue := r1.blue + r2.blue, green := r1.green + r2.green, red := r1.red + r2.red }

[James Sully]

thank you!