The Coq mailing list

[Benjamin Pierce <bcpierce AT cis.upenn.edu>]

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
> 
>