Def ToAdditive.reorderForall

Modification history

2025-08-12 21:40
Mathlib/Tactic/ToAdditive/Frontend.lean
feat: deprecate `str` syntax for `to_additive` docstrings in Mathlib (#28135) …
Deleted ToAdditive.reorderForallView on Github →
2024-07-15 23:26
Mathlib/Tactic/ToAdditive.lean
feat(to_additive): unfold lemmas generated by `simp` (#14628) …
Modified ToAdditive.reorderForallView on Github →
2023-04-28 06:56
Mathlib/Tactic/ToAdditive.lean
perf: improve performance of `to_additive` (#3632) …
Modified ToAdditive.reorderForallView on Github →
2022-12-02 17:02
Mathlib/Tactic/ToAdditive.lean
feat: to_additive can reorder arguments of generated declaration (#818) …
Added ToAdditive.reorderForallView on Github →