Zulip Chat Archive

Stream: maths

Topic: char_zero and char_p

Yury G. Kudryashov (Oct 18 2020 at 18:09):

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 (Oct 19 2020 at 07:47):

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

Johan Commelin (Oct 19 2020 at 07:47):

char_zero is older

Johan Commelin (Oct 19 2020 at 07:48):

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

Last updated: Dec 20 2023 at 11:08 UTC