Hi,

I am experimenting with the rewrite rules to be introduced in future Coq 8.20 .

The following code does not parse, with the following error : `Error: Syntax error: '==>' expected after [rw_pattern] (in [rewrite_rule]).`

```
From mathcomp Require Import ssrbool.
Symbol pplus : nat -> nat -> nat.
Notation "a ++ b" := (pplus a b).
Rewrite Rule pplus_rewrite :=
| ?n ++ 0 ==> ?n
| ?n ++ S ?m ==> S (?n ++ ?m)
| 0 ++ ?n ==> ?n
| S ?n ++ ?m ==> S (?n ++ ?m).
```

ssrbool defines `==>`

as a *reserved* notation, and this confuses the parser. And per https://coq.inria.fr/doc/master/refman/user-extensions/syntax-extensions.html?highlight=notation#enabling-and-disabling-notations , reserved notations cannot be disabled, so `Disable Notation "==>" (all).`

is inoperent.

Do you have any suggestion? Shall this be reported through GitHub or moved to coq-devs zulip channel?

Thanks

Sorry for the late reply. I have a PR to replace `==>`

with `>->`

since this should have fewer conflicts (#18808)

Why not just `=>`

? (like in the match construct)

Pierre Roux said:

Why not just

`=>`

? (like in the match construct)

This approach is likely to be free of future conflicts, isn't it?

Sounds much more robust to me yes.

Looking at the patch, it seems >-> is used also for coercions. Wouldn't the proposed patch conflicts there? (I acknowledge

a rewrite rule on a term with coercions could be meaningless, but never doubt user's inventiveness)

`>->`

is used in the Coercion command and in the Rewrite Rule command, they're separate commands so no conflict

Make sense, thanks.

For the record, there are instances of notations with `>->`

, with other tokens. involved I am the opinion that these notations should not interfere, but it is worth a second opinion.

```
jjhugues@mac-pepperapple coq % grep -r ">->" . |grep Nota
./math-comp/mathcomp/fingroup/morphism.v:Notation "{ 'morphism' D >-> T }" := (morphism_for D (Phant T))
./coq/theories/ssr/ssrfun.v:Reserved Notation "{ 'morph' f : x / a >-> r }" (at level 0, f at level 99,
./coq/theories/ssr/ssrfun.v:Reserved Notation "{ 'morph' f : x y / a >-> r }" (at level 0, f at level 99,
./coq/theories/ssr/ssrfun.v:Reserved Notation "{ 'homo' f : x / a >-> r }" (at level 0, f at level 99,
./coq/theories/ssr/ssrfun.v:Reserved Notation "{ 'homo' f : x y / a >-> r }" (at level 0, f at level 99,
./coq/theories/ssr/ssrfun.v:Reserved Notation "{ 'mono' f : x / a >-> r }" (at level 0, f at level 99,
./coq/theories/ssr/ssrfun.v:Reserved Notation "{ 'mono' f : x y / a >-> r }" (at level 0, f at level 99,
./coq/theories/ssr/ssrfun.v:Notation "{ 'morph' f : x / a >-> r }" :=
./coq/theories/ssr/ssrfun.v:Notation "{ 'morph' f : x y / a >-> r }" :=
./coq/theories/ssr/ssrfun.v:Notation "{ 'homo' f : x / a >-> r }" :=
./coq/theories/ssr/ssrfun.v:Notation "{ 'homo' f : x y / a >-> r }" :=
./coq/theories/ssr/ssrfun.v:Notation "{ 'mono' f : x / a >-> r }" :=
./coq/theories/ssr/ssrfun.v:Notation "{ 'mono' f : x y / a >-> r }" :=
```

those are parenthesized so don't interfere

Jerome Hugues has marked this topic as unresolved.

I think you need to write your own logic for this. Something like `multimatch goal with H : _ |- _ => exact H end`

Gaëtan Gilbert said:

I think you need to write your own logic for this. Something like

`multimatch goal with H : _ |- _ => exact H end`

Does this apply to this discussion thread @Gaëtan Gilbert ?

no, should be https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Backtracking.20and.20assumption.20.28without.20using.20Ltac.29

Last updated: Jun 22 2024 at 14:01 UTC