I'm following instructions in https://www.cis.upenn.edu/~bcpierce/sf/current/Imp.html, and trying to define a new notation |\. (Instead of ||, which is used in the webpage but seems to be interpreted as an OR operator by my coq)
Reserved Notation "e |\ n" (at level 50, left associativity).
However coq still thinks that |\ is an undefined operator.
Inductive aevalR : aexp -> nat -> Prop :=
| E_ANum : forall n : nat, (ANum n) |\ n.
Error: Unknown interpretation for notation "_ |\ _".
My coq version is 8.4pl6(Nov. 2015). How can I make coq accept my new |\ operator?