abel tactic

Stream: general

[Mario Carneiro]

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 nat.cast and int.cast in norm_num, but otherwise it is full featured using +, -, and add_monoid.smul, gsmul.

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]

Great! How far is the module version then?

[Mario Carneiro]

The module version is basically a combination of abel and 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