derive add_comm_monoid

Stream: general

[Daniel Selsam]

Could somebody briefly explain how @[derive [add_comm_monoid]] works, and point me to the code that actually executes?

[Gabriel Ebner]

It's probably the δ-derive handler: https://github.com/leanprover-community/mathlib/blob/768980a90c2bdf2b4ad957efcd2f4c86c60be262/src/tactic/delta_instance.lean