mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(Tactic/ToAdditive): split implementation from the attribute

Open fpvandoorn opened this issue 3 years ago • 0 comments
trafficstars

  • This way we can add @[to_additive] attributes much easier via metaprogramming.
  • Useful for the @[simps] attribute

fpvandoorn avatar Oct 13 '22 15:10 fpvandoorn