field already declared

Stream: new members

[Horatiu Cheval]

I am trying to define a small algebraic hierarchy from scratch following the way it's done in mathlib and I get this error.

class monoid (M : Type*) extends has_mul M, has_one M :=
(mul_assoc : ∀ x y z : M, x * (y * z) = (x * y) * z)
(mul_one : ∀ x : M, x * 1 = x)
(one_mul : ∀ x : M, 1 * x = x)

class comm_monoid (M : Type*) extends monoid M :=
(mul_comm : ∀ x y : M, x * y = x * y)

class group (G : Type*) extends monoid G, has_inv G :=
(mul_left_inv : ∀ x : G, x⁻¹ * x = 1)

class comm_group (G : Type*) extends group G, comm_monoid G

--invalid 'structure' header, field 'to_monoid' from 'hidden.comm_monoid' has already been declared

I assume it's because both group and comm_monoid have to_monoid fields, but how do I fix it?

[Johan Commelin]

You can use

set_option old_structure_cmd true

before your code

[Johan Commelin]

This will merge the fields that both parents have in common

[Johan Commelin]

But the structures that you extend should also be "old" structures. So you have to set the option all the way at the top

[Horatiu Cheval]

Oh, I see, I missed that from the mathlib source files. Thanks!