Topic: abel tactic
Mario Carneiro (Sep 10 2018 at 07:28):
Say hello to the
abel tactic, which does the same thing as
ring but for commutative additive monoids and commutative groups. It doesn't currently support
* on rings, since it would require a bit more support for
norm_num, but otherwise it is full featured using
I'm sure it won't be long before someone asks me to make a multiplicative version, I'll look into it. I plan to just use
additive to get the multiplicative version.
Patrick Massot (Sep 10 2018 at 07:31):
Great! How far is the module version then?
Mario Carneiro (Sep 10 2018 at 07:34):
The module version is basically a combination of
ring. It might be possible to generalize the coefficient ring to uniformize the treatment of additive groups as Z-modules, but we will need semimodules first, or else we will lose support for additive monoids with such a generalization
Last updated: May 10 2021 at 18:22 UTC