## Stream: general

#### Johan Commelin (Dec 11 2020 at 08:02):

Do simps and to_additive play well together?

/-- Composition of monoid morphisms (monoid_hom.comp) as a monoid morphism. -/
(add_monoid_hom.comp) as an additive monoid morphism."]
def comp_hom [monoid M] [comm_monoid N] [comm_monoid P] :


this generate monoid_hom.comp_hom_apply_apply but the additive version seems to be missing.

#### Eric Wieser (Dec 11 2020 at 08:09):

What order do the attributes execute in? Is it left to right, or the reverse order like python?

#### Reid Barton (Dec 11 2020 at 12:32):

to_additive should be last (https://leanprover-community.github.io/mathlib_docs/attributes.html#to_additive)
but there's also a fixed list of attributes that it copies somewhere, I think

#### Floris van Doorn (Dec 12 2020 at 01:05):

This can easily be implemented by adding simps to this list: https://github.com/leanprover-community/mathlib/blob/master/src/algebra/group/to_additive.lean#L296

#### Kevin Buzzard (Dec 12 2020 at 01:22):

Can this issue also be solved relatively simply?

#### Floris van Doorn (Dec 12 2020 at 01:29):

I think it already does that if you give an @[ancestor] attribute:
https://github.com/leanprover-community/mathlib/blob/master/src/algebra/group/defs.lean#L64-L70

#### Bryan Gin-ge Chen (Dec 12 2020 at 04:09):

We have a related open issue #1639.

#### Johan Commelin (Dec 12 2020 at 04:14):

hmm, is it still true that to_additive shouldn't be used for structures? because that suggests I need a different way of fixing the issue, namely by manually defining add_monoid_hom.comp_hom.

#### Floris van Doorn (Dec 12 2020 at 04:47):

You are using to_additive for an object in a structure, which I think was always fine.

Done in #5331.

#### Yury G. Kudryashov (Dec 12 2020 at 19:12):

to_additive can't generate structure or class definitions.

#### Yury G. Kudryashov (Dec 12 2020 at 19:12):

E.g., it can't generate class add_group from class group.

Last updated: May 14 2021 at 12:18 UTC