The Coq mailing list

[Adam Megacz <megacz AT cs.berkeley.edu>]

Is there any way to have a [Notation] whose definition involves
parameters of the Record/Class currently being defined?

Example:

  Class Monoid (Carrier:Set)(mult:Carrier->Carrier->Carrier) :=
  { neutral : Carrier
  ; identL  : forall a,     (mult a neutral) = a
  ; identR  : forall a,     (mult neutral a) = a
  ; assoc   : forall a b c, (mult a (mult b c)) = (mult (mult a b) c)
  }.

I would much rather write this (especially for classes which are more
complicated than a simple Monoid), but Coq won't accept it:

  Reserved Notation "a ** b" (at level 50).
  Class Monoid (Carrier:Set)(mult:Carrier->Carrier->Carrier) :=
  { neutral : Carrier
  ; identL  : forall a,     a**neutral = a
  ; identR  : forall a,     neutral**a = a
  ; assoc   : forall a b c, a**(b**c) = (a**b)**c
  } where "a ** b" := (mult a b).

I tried putting the 'where "a ** b" := (mult a b)' in a few other places
to no avail.  Unfortunately due to other constraints I can't just add a
new field and a notation for it, like this:

  Class Monoid (Carrier:Set)(mult:Carrier->Carrier->Carrier) :=
  { mult_again := mult where "a ** b" := (mult_again a b)
  ...
  }

By the way, the definition above is technically illegal according to the
Coq manual (you're not supposed to be able to put "where" after a ":="
clause according to a strict reading of the BNF) but Coq 8.2pl3 accepts
it anyways.  Not sure if the BNF should be more permissive or Coq should
be stricter.

Thanks,

  - a