The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

On Tue, 13 Dec 2011 16:54:09 +0100, Nuno Gaspar 
<nmpgaspar AT gmail.com>
 wrote:
Non-text part: multipart/alternative
> > Class Arrow (X:Type) (Y:Type) := {
> >  arrow : X -> Y
> > }.
> >
> > Instance AX1 : Arrow X x := { arrow := projectionX }.
> > Instance AX1 : Arrow Y y := { arrow := projectionY }.
> >
> > Notation "e '->x'" := (arrowX e) (at level 80, right associativity).
> >
> > But I wouldn't recommend such a notation, since I would fear to confuse
> > the parser.
> >
> 
> Ok, I guess i'm stuck with the % notation then.

I think this comment was directed at the precise notation you used,
rather than at having some notation like this in general. This is
simply becuase ->x is valid syntax by default, and so would be
confusing. In particular, I would guess that it would make '-> x' and
'->x' mean different things.

  Tom