Stream: Coq users

Topic: ✔ Coq 8.20 rewrite rules and reserved notations from ssrbool


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

view this post on Zulip Notification Bot (Mar 15 2024 at 13:02):

Jerome Hugues has marked this topic as resolved.

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

view this post on Zulip 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: Jun 23 2024 at 04:03 UTC