The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

There is some special handling of patterns `{ one_nonterminal }` in a constr 
notation.
I don't know much about it (I just grepped `"{"` in the code) but at least in 
your example it seems to be possible to work around it with an auxiliary custom entry:

    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.

    Declare Custom Entry foo_aux.

    Notation "<{ x }>" := x
      (x custom foo_aux) : foo_scope.

    Notation "{ P } e { Q }" :=
      ("<{ {" ++ P ++ "} " ++ e ++ " {" ++ Q ++ "} }>")%string
        (in custom foo_aux,
            e custom foo,
            P custom foo,
            Q custom foo) : foo_scope.

    (* works  *)
    Compute ( <{ { * } * { * } }> ).


Gaëtan Gilbert

On 22/10/2023 17:50, Benjamin Pierce wrote:
> 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 ( <{ { * } * { * } }> ).