coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Arthur Chargu�raud <arthur.chargueraud AT inria.fr>
- To: coq-club AT inria.fr
- Cc: Benjamin Pierce <bcpierce AT cis.upenn.edu>
- Subject: Re: [Coq-Club] yet another pb with Notation (from Init/Logic.v)
- Date: Sat, 15 May 2010 10:05:49 +0200
> 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
- [Coq-Club] record field is "lost" if import is used, Patrice Chalin
- Re: [Coq-Club] record field is "lost" if import is used,
Hugo Herbelin
- [Coq-Club] yet another pb with Notation (from Init/Logic.v),
Jean-Francois Monin
- Re: [Coq-Club] yet another pb with Notation (from Init/Logic.v),
Hugo Herbelin
- Re: [Coq-Club] yet another pb with Notation (from Init/Logic.v), Dan Colish
- Re: [Coq-Club] yet another pb with Notation (from Init/Logic.v),
Benjamin Pierce
- Re: [Coq-Club] yet another pb with Notation (from Init/Logic.v), Arthur Charguéraud
- Re: [Coq-Club] yet another pb with Notation (from Init/Logic.v), Benjamin Pierce
- Re: [Coq-Club] yet another pb with Notation (from Init/Logic.v), Arthur Charguéraud
- Re: [Coq-Club] yet another pb with Notation (from Init/Logic.v),
Hugo Herbelin
- [Coq-Club] yet another pb with Notation (from Init/Logic.v),
Jean-Francois Monin
- Re: [Coq-Club] record field is "lost" if import is used,
Hugo Herbelin
Archive powered by MhonArc 2.6.16.