The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

Hi Coq-Club !

I would like to know whether it is possible to include pattern inside
notations.

More specifically, I have some monadic code, where I use the common do
notation:

Notation "'do' X <- A ; B" := (bind (fun X => B) A)
   (at level 200, X ident, A at level 100, B at level 200).

I would like to write something like :

Notation "'do' P <- A ; B" := (bind (fun X => let 'P := X in B) A)
    (at level 200, X ident, A at level 100, B at level 200).

Where P is a general pattern. This previous code is accepted by Coq.
However, it does not do what I want: when I type

do (a, b) <- blah; blih

it refuses it, while I would expect it to translate it to:

bind (fun X => let '(a, b) := X in blih) blah

Any ideas ?

-- 
JH Jourdan

Attachment: signature.asc
Description: OpenPGP digital signature