Topic: char_zero and char_p
Yury G. Kudryashov (Oct 18 2020 at 18:09):
What do you think about the following refactor?
- make it work for an
add_monoidinstead of a
char_p α 0instead of
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: May 10 2021 at 08:14 UTC