Subject: Notation which uses parameters of a Record/Class? Newsgroups: gmane.science.mathematics.logic.coq.club Date: Wednesday 14th April 2010 04:06:45 UTC (over 8 years ago) 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 |
|||