The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

So yeah, David Perreira gave me the solution offline, and it turns out that there is an example in [1].

The need for the explicit use of the % syntax rapidly becomes overkill, I would expect type inference to go further on this matter. 

Anyway, it works for my purposes, but If anyone has ideas on how to avoid this, please, don't be shy :)


[1] http://adam.chlipala.net/cpdt/html/Extensional.html

2011/12/13 Nuno Gaspar <nmpgaspar AT gmail.com>

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!







--
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.

-- 
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.