The Coq mailing list

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

Thanks to everybody for all the suggestions!  I finally ended up going with 
the simplest one: keeping the double-brackets and hacking the html output to 
reduce the space between them.  Those interested can check out how it works 
in context here:

   http://www.seas.upenn.edu/~cis500/current/sf/Hoare.html

I wasn't satisfied with notations that required prefixing because I want to 
use the same notation for "embedded annotations" inside programs:

   http://www.seas.upenn.edu/~cis500/current/sf/Hoare2.html

Same consideration applies to Greg's suggestion not to use any notation at 
all.

For an application that didn't involve lots of newbies with all sorts of 
different machine / ide configurations, Unicode might indeed be the best 
solution...

    - Benjamin


On Mar 8, 2013, at 7:48 PM, CJ Bell 
<siegebell AT gmail.com>
 wrote:

> The problem with my solution is that you must write "|-{P} (1+2) {Q}"
> instead of "|-{P} 1+2 {Q}". Parentheses are always required around the
> command in the center because of the way that functions are parsed :/
> 
> 
> -cj
> 
> 
> 
> On Fri, Mar 8, 2013 at 7:07 PM, CJ Bell 
> <siegebell AT gmail.com>
>  wrote:
>> Here is an approach that works because it uses the existing notation
>> for " { } " and requires prefixing Hoare triples with "|-" (or some
>> other keyword). Hard to tell if it breaks something, though.
>> 
>> 
>> Inductive ht_pred : Set := ht_pred_: nat->ht_pred.
>> Inductive ht : ht_pred->nat->ht_pred->Prop := .
>> 
>> Delimit Scope htriple with htriple.
>> Delimit Scope htriple_pred with htriple_pred.
>> Arguments ht P%htriple_pred c%nat Q%htriple_pred.
>> 
>> Module Notations.
>>  Notation " { P } " := (ht_pred_ P%nat) : htriple_pred.
>>  Notation "|-" := ht (no associativity, at level 0) : htriple.
>> End Notations.
>> 
>> Module TestNotations.
>>  Import Notations.
>>  Open Scope htriple.
>> 
>>  (* do existing notations still work? *)
>>  Record Rat : Set := mkRat {
>>    top: nat; bottom: nat; Rat_cond: (gt bottom O) }.
>>  Goal (forall b:bool, { b=true } + { b=false }). destruct b; auto. Qed.
>>  Goal {a | a<>false}. exists true; intro; discriminate. Qed.
>> 
>>  Goal (forall p, {p}%htriple_pred = ht_pred_ p). reflexivity. Qed.
>> 
>>  Goal (forall p c q,
>>    |- {p} c {q} <-> ht (ht_pred_ p) c (ht_pred_ q)).
>>  Proof. split; intros; auto. Qed.
>> 
>> End TestNotations.
>> 
>> 
>> 
>> -cj