coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Benjamin Pierce <bcpierce AT cis.upenn.edu>
- To: Arthur Chargu�raud <arthur.chargueraud AT inria.fr>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] yet another pb with Notation (from Init/Logic.v)
- Date: Sat, 15 May 2010 10:31:23 -0400
Thanks, Arthur.
This is a nice technique in general, but for Software Foundations I'm not
satisfied with it: since this is an introductory course, having two sets of
notations (one for blackboard discussions, one for Coq) is very confusing.
So I'd really prefer to use notations that will work for both purposes.
An alternative that we're just beginning to look at seriously is using
unicode notations, but we're not completely sure that the world is ready for
this...
- Benjamin
On May 15, 2010, at 4:05 AM, Arthur Charguéraud wrote:
>
>> 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.