The Coq mailing list

[Arthur Chargu�raud <arthur.chargueraud AT inria.fr>]

> By the way, since this conversation started with the way we use notations 
> in the Software Foundations materials, I should say that we're very open to 
> better suggestions about how to use notations so they (look nicer and/or) 
> don't conflict with standard library stuff...
>
>     - Benjamin

One trick I have used extensively in my recent developments to avoid
conflicts with the
standard library is to have either a quote or a backslash in front of
the leading symbol
of each of my notation. Examples:

\if b then e1 else e2

\fun x => t

\let x := t

t1 \; t2

E \u F

E \n F

You can also play a similar trick using a quote symbol, as I did
http://www.chargueraud.org/arthur/research/2009/deep/src/DeepPrinter.v.html
In this particular development, I placed a quote in front of every keyword.
This strategy greatly reduces the possibiliy for parsing conflicts.
The result looks like this:

'if b 'then t1 'else t2

'fun x '-> t

'fun x1 x2 x3 '-> t

'function '| p1 '-> t1 '| p2 '-> t2

'match t 'with '| p1 '-> t1 '| p2 '-> t2

#(x,y)

For tuples I have used a sharp symbol because '(x,y) is already used
by let patterns from Coq.
Remark: the use of quotes is not incompatible with
the use of variables named with a training quote (e.g., x').

Hope it helps,

+
Arthur