Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] yet another pb with Notation (from Init/Logic.v)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] yet another pb with Notation (from Init/Logic.v)


chronological Thread 
  • 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





Archive powered by MhonArc 2.6.16.

Top of Page