mathlib
afec1d73 - fix(tactics/alias): Make docstring calculation available to to_additive (#13968)

Commit
3 years ago
fix(tactics/alias): Make docstring calculation available to to_additive (#13968) PR #13944 fixed the docstrings for iff-style aliases, but because of code duplication I added in #13330 this did not apply to aliases introduced by `to_additive`. This fixes that.
Author
Parents
Loading