The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You can hack something together using typeclasses.  See https://coq.inria.fr/bugs/show_bug.cgi?id=3090, a feature request I made to make the hack unnecessary, for a proof of concept.

-Jason

On Monday, August 26, 2013, t x wrote:

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!