The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

Le Tue, 13 Dec 2011 10:41:03 +0100,
Nuno Gaspar 
<nmpgaspar AT gmail.com>
 a écrit :

> Hello.
> 
> So I would like to use the same syntactical operator for different
> types. For instance,
> 
> Inductive foo : X :=
>    | Cons : x -> y -> z -> foo.
> 
> And now assume that the projections are properly defined, and then
> 
> Notation "e '->x' " := (projectionX e) (at level 80, right
> associativity). ...
> 
> Now, I want to define another inductive, and use the same "->"
> operator, but that will not work unless I explicitly use scopes.
> 
> Something like:
> 
> Notation "e '->x' " := (projectionX e) (at level 80, right
> associativity) : foo_scope.
> 
> But then again, that really does not absolutely solve my problem since
> now I _explicitly_ need to open/close scopes, which means that I
> cannot use the intended overloaded operator "->" in the same
> context...
> 
> So, how does one achieve that? :-)
> 
> thank you!
> 
Maybe you could put your two inductives into a same type class?

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.