The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

2011/12/13 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?

From [*], The status of Type Classes is experimental. :)

Anyway, I'll look into it. thank you.
 
[*]http://coq.inria.fr/refman/Reference-Manual024.html

 

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.

-- 
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.