Zulip Chat Archive

Stream: new members

Topic: field already declared


Horatiu Cheval (Feb 17 2021 at 08:25):

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 (Feb 17 2021 at 08:26):

You can use

set_option old_structure_cmd true

before your code

Johan Commelin (Feb 17 2021 at 08:27):

This will merge the fields that both parents have in common

Johan Commelin (Feb 17 2021 at 08:27):

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 (Feb 17 2021 at 08:28):

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


Last updated: Dec 20 2023 at 11:08 UTC