Zulip Chat Archive

Stream: new members

Topic: field already declared


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Feb 17 2021 at 08:26):

You can use

set_option old_structure_cmd true

before your code

view this post on Zulip Johan Commelin (Feb 17 2021 at 08:27):

This will merge the fields that both parents have in common

view this post on Zulip 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

view this post on Zulip Horatiu Cheval (Feb 17 2021 at 08:28):

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


Last updated: May 18 2021 at 17:44 UTC