The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

  Here is my minimal fail case:
https://gist.github.com/anonymous/09bf33154f6f3e1e0573

  In short, I want to create a notation which does _different_ things based on the type of the arguments capture.

In particular, I want:

"START 20 END => pZ 20"

"START true END => pBool true"

So I know that I can define a

Notation "'STARTZ' x 'ENDZ'" = (pZ x)

Notation "'STARTB' x 'ENDB'" = (pBool x)

However, I'd prefer to have one definition of "START x END", and have it do different things based on the type. Is this possible in COq?

Thanks!