Zulip Chat Archive

Stream: general

Topic: abel tactic


view this post on Zulip 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 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.

view this post on Zulip Patrick Massot (Sep 10 2018 at 07:31):

Great! How far is the module version then?

view this post on Zulip Mario Carneiro (Sep 10 2018 at 07:34):

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


Last updated: May 10 2021 at 18:22 UTC