The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

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