Zulip Chat Archive

Stream: maths

Topic: char_zero and char_p


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

view this post on Zulip Gabriel Ebner (Oct 19 2020 at 07:47):

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

view this post on Zulip Johan Commelin (Oct 19 2020 at 07:47):

char_zero is older

view this post on Zulip 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: May 10 2021 at 08:14 UTC