coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Guillaume Brunerie <guillaume.brunerie AT gmail.com>
- To: Mehdi Dogguy <mehdi AT dogguy.org>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Notation with "Type"
- Date: Wed, 8 Jun 2011 18:49:13 +0200
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=SUzkjSpFUc3St0kbbFpo0eaYE4ZSofjl7xNAtnC+szhaTh8mWH2Lu6Jrxdoohz3c96 5d1oVzrmrKKpW9092mqFfi9ZMp7JB/i7rMkqmcBo4RPEuah6CtMOsZ2vR7w4Ova0XePn mJ2R8D8uRNPxkgym/1AM/kaDn5ZhYcU7fe75E=
2011/6/8 Mehdi Dogguy <mehdi AT dogguy.org>
On 08/06/2011 17:03, Guillaume Brunerie wrote:I could be wrong but isn't "Definition s := f Type" enough for your needs?
> The following does not work as expected:
>
> Parameter f : Type -> Type.
>> Notation s := (f Type).
>> Check s.
>>
>
(why do you need Notation?)
Indeed, but in my case what I actually want is "Notation "#s" := (f Type)", because this term has a special meaning and I want to distinguish it from the other identifiers in the script.
I could have written "Definition __s := (f Type)", or something like that, but I find "#s" prettier than "__s" (and I need "Notation" for that).
- [Coq-Club] Notation with "Type", Guillaume Brunerie
- Re: [Coq-Club] Notation with "Type",
AUGER Cedric
- Re: [Coq-Club] Notation with "Type", Guillaume Brunerie
- Re: [Coq-Club] Notation with "Type",
Mehdi Dogguy
- Re: [Coq-Club] Notation with "Type", Guillaume Brunerie
- Re: [Coq-Club] Notation with "Type", Hugo Herbelin
- Re: [Coq-Club] Notation with "Type", Guillaume Brunerie
- Re: [Coq-Club] Notation with "Type",
AUGER Cedric
Archive powered by MhonArc 2.6.16.