Say I have a relation and its reflexive and transitive closure (with n counting the number of "transitive steps":
Variable A: Type.
Inductive Relation: A -> A -> Prop :=
| rel: forall (a b: A), Relation a b.
Notation "a --> b" := (Relation a b) (at level 50).
Inductive Refl_Trans_Rel: A -> A -> nat -> Prop :=
| zero_step: forall a b, a --> b -> Refl_Trans_Rel a b 0
| n_steps: forall a b c n, a --> b /\ Refl_Trans_Rel b c n
-> Refl_Trans_Rel a c (S n).
Now, I want to have a notation similiar as a --> b:
Notation "a -->^ n b" :=
(Refl_Trans_Rel a b n) (at level 50, n at next level, b at next level).
For printing, there is no problem: Check forall a b n, Refl_Trans_Rel a b n. indeed prints:
forall (a b : A) (n : nat), a -->^ n b
: Prop
However, when I want to use the notation myself, there is a problem:
Check forall a b n, a -->^ n b.
fail with:
Syntax error: [constr:operconstr] expected after [constr:operconstr]
(in [constr:operconstr]).
Any idea of why it fails ?
P.S.: feel free to edit the title with something more precise, since I have no idea of the cause, I have no idea for a better title.
It seems that Coq is trying to parse the n b part in a -->^ n b as a function application. One way of overcoming this difficulty would be to put n at a lower level, like so:
Notation "a -->^ n b" := (Refl_Trans_Rel a b n) (at level 50, n at level 9).
Check forall (a b : A) (n : nat), a -->^ n b.
Another option is to put a separator between b and n:
Notation "a --> b # n" := (Refl_Trans_Rel a b n) (at level 50).
Check forall (a b : A) (n : nat), a --> b # n.
You can find out more about notations and parsing levels here.