list auto coercions of old structures

Stream: general

[Yury G. Kudryashov]

Hi, can I quickly get the list of the auto generated coercions for an old structure? I want something like

> env.get_coercions `comm_semigroup
[`comm_semigroup.to_semigroup]

I see env.structure_fields, and it includes autogenerated coercions for new-style structures but for comm_semigroup it returns [mul, mul_assoc, mul_comm].

[Yury G. Kudryashov]

I rewrote to_additive to automatically take care of structure fields and things like cases_on, _proof_1 etc. Now coercions like comm_semigroup.to_semigroup is the last thing to_additive can't find automatically when it sees @[to_additive add_comm_semigroup] class comm_semigroup ...

[Andrew Ashworth]

Does tactic.algebra not solve your problems?

[Yury G. Kudryashov]

@Andrew Ashworth It still depends on manual input of ancestry information. Though it's definitely better to have it once than twice, I'd prefer Lean to make this information available using some meta constant.

[Johan Commelin]

@Fabian Glöckle was also looking for something like this. I don't think he found a solution.