char_zero and char_p

Stream: maths

[Yury G. Kudryashov]

What do you think about the following refactor?

• make p in char_p an out_param;
• make it work for an add_monoid instead of a semiring;
• use char_p α 0 instead of char_zero?

I'm not going to do it any time soon, but if you like it, then I'll add an issue.

[Gabriel Ebner]

I was very surprised when I first saw that they're different definitions.

[Johan Commelin]

char_zero is older

[Johan Commelin]

I'm still scared of out_params... but if it works, that would be cool!