The Coq mailing list

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

Thanks, Cédric (and Arthur, who wrote offline with similar suggestions)!

I do want to stay with ascii, to avoid forcing too many people to struggle 
with how to edit unicode.  But the other solutions do seem pretty reasonable 
-- my current favorite is [{P} c {Q}].  Another option we're considering is 
to keep {{P}}c{{q}} but fix up the HTML output so that the braces come out 
close together.  

I'm still hoping someone will tell me that it's possible to make {P}c{Q} 
work… :-)

    - B


On Mar 8, 2013, at 12:54 PM, AUGER Cédric 
<sedrikov AT gmail.com>
 wrote:

> Le Fri, 8 Mar 2013 12:02:19 -0500,
> "Benjamin C. Pierce" 
> <bcpierce AT cis.upenn.edu>
>  a écrit :
> 
>> In the Software Foundations text, we are currently using the notation
>> 
>>   {{P}} c {{Q}}
>> 
>> for Hoare triples, which is not completely awful but rather heavy.
>> Is it hopeless to dream that we might somehow be able to get Coq's
>> Notation mechanism to accept the standard notation
>> 
>>   {P} c {Q}
>> 
>> or something similar?
> 
> That depends on what you mean with similar…
> 
> <P> c <Q>
> '{ ' P ' }' c '{ ' Q ' }'
>   -- using unbreakable spaces (not sure it works)
> «P» c «Q»
> ⦃ P ⦄ c ⦃ Q ⦄
> P ⊢ c ⇒ Q
> 
> using unicode, there are many solutions…
> 
> Now if you want to stay in ASCII domain, well, maybe something like:
> '[{' P '}' c '{' Q '}]' or
> '<{' P '}' c '{' Q '}>'
> (I mean to enclose the statement with an opening stuff and a closing
> one, [{P} c {Q}] or <{P} c {Q}> being a little smaller than your
> original notation)
> 
>> 
>> Thanks
>> 
>>    - Benjamin
>> 
>> 
>