Jerome Hugues (Mar 15 2024 at 13:01): Jerome Hugues (Mar 15 2024 at 13:01):Thanks. The issue is solved as far as Zulip is concerned. Waiting for the PR to be accepted. Thanks all for your clarifications on this.
Notification Bot (Mar 15 2024 at 13:02):Jerome Hugues has marked this topic as resolved.
Pierre Roux (Mar 15 2024 at 13:37):Gaëtan Gilbert said:
>->is used in the Coercion command and in the Rewrite Rule command, they're separate commands so no conflict
Sure, my concern was rather about a potential user puting the token in a notation that could conflict (just like ==> previously). It just seems that the fun and match construct being much more pervasive than coercion declarations, that risk is much lower with => compared to >->.
Yann Leray (Mar 15 2024 at 19:07):Pierre Roux said:
Why not just
=>? (like in the match construct)
Now I wonder why I felt like this was a bad idea in the first place? I don't feel like I should be the one to choose what this should be in the end, I don't have enough data.
Last updated: Oct 13 2024 at 01:02 UTC