The Coq mailing list

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

Dear Coq folk,

I'm having my every-couple-of-years try at making the Imp and Hoare logic notations nicer in Software Foundations.  At the moment, we use

   <{ c }>

for bare Imp commands and 

   {{P}} c {{Q}}

for Hoare triples.  I'd like to change the latter to 

   <{ {P} c {Q} }>

but this doesn't appear to work, as the simple experiment below shows.  Indeed, it appears that the curly braces are actually the problem (replacing them with parens gives the result I expected).   

Many thanks for any insight or advice,

   - Benjamin

From Coq Require Import Strings.String. Import String.

Declare Custom Entry foo.
Declare Scope foo_scope.
Open Scope foo_scope.

Notation "*" :=
  "*"%string (in custom foo)
    : foo_scope.

(* Defining a "hoare triple like" notation with parens works: *)
Notation "<{ ( P ) e ( Q ) }>" :=
  ("<{ (" ++ P ++ ") " ++ e ++ " (" ++ Q ++ ") }>")%string
    (e custom foo,
      P custom foo,
      Q custom foo) : foo_scope.
Compute ( <{ ( * ) * ( * ) }> ).

(* But doing the same thing with curly braces does not: *)
Notation "<{ { P } e { Q } }>" :=
  ("<{ {" ++ P ++ "} " ++ e ++ " {" ++ Q ++ "} }>")%string
    (e custom foo,
      P custom foo,
      Q custom foo) : foo_scope.
(* Syntax error here: *)
Compute ( <{ { * } * { * } }> ).