The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

You need to put the single quotes:

Notation "A 'ε ' b" := (epsilon A b)  (at level 70). 

Cheers

2014-09-19 14:50 GMT+02:00 Richard Dapoigny <richard.dapoigny AT univ-savoie.fr>:

Hi all,
I have the following trouble with notation on my Windows system.
I define the following notation:
=========================
Class N : Type.
Class epsilon (A a:N) : Prop.

Notation "A ε b" := (epsilon A b)  (at level 70).
...
=========================
and I obtain the following error:
Error: A notation must include at least one symbol.
The same program correctly runs on a Mac.
If someone has an idea?
Thanks in advance,
Richard

--

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.