Home Reading Searching Subscribe Sponsors Statistics Posting Contact Spam Lists Links About Hosting Filtering Features Download Marketing Archives FAQ Blog From: AUGER =?ISO-8859-1?B?Q+lkcmlj?= lri.fr> Subject: Re: Notation which uses parameters of a Record/Class? Newsgroups: gmane.science.mathematics.logic.coq.club Date: Wednesday 14th April 2010 07:14:01 UTC (over 8 years ago) ```Le Wed, 14 Apr 2010 04:06:45 +0000, Adam Megacz a écrit : > > 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 > I think, this is half satisfactory... Reserved Notation "a ** b" (at level 50). Section Monoid. Variable Carrier: Set. Variable mult_monoid: Carrier -> Carrier -> Carrier. (* The trick is to put mult_monoid at toplevel, * as you did with your mult_again, but without * the need to redefine it *) Notation "a ** b" := (mult_monoid a b). Class Monoid := { 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) }. End Monoid. (* At end of the section all variables are generalized, * as you whish, but Notation die with it. * The result is that you have been able to use Notation * to define Monoids, but you won't use them later. * Note, that you weren't forced to reserve a Notation, * but as you will probably redefine it later, * you won't have to define level each time. *) Print Monoid. (* You can see, you lose your Notation. *)```
CD: 27ms