The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

Hi,

Using Coq 8.4 I define a typeclass just for overloading an infix
notation for application:

  Class Applic (A: Set) := { app: A -> A -> A} .
  Notation "m @ n" := (app m n) (at level 90, no associativity).

Here is an instance of this typeclass:

   Inductive Map: Set := mx0: Map | mx1: Map | mapp: Map -> Map -> Map.
   Instance Applic_Map : Applic Map := { app m n := mapp m n }.

The infix notation seems to work for this instance:

   Check (mx0 @ mx1).

But when I try to define a size function for Map, the overloaded
syntax is not accepted in a pattern:

   Fixpoint MapSize (m:Map) {struct m} : nat :=
   match m with
   | mx0 => 0
   | mx1 => 0
   | (m1 @ m2) => S ((MapSize m1) + (MapSize m2))
   end.

   Toplevel input, characters 83-90:
   Error: Invalid notation for pattern.

What is the problem?  If I explicitly make a notation for the type Map

   Notation "m @ n" := (mapp m n) (at level 90, no associativity).

the pattern match is accepted.

Randy