coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Guillaume Brunerie <guillaume.brunerie AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Notation with "Type"
- Date: Wed, 8 Jun 2011 17:03:57 +0200
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:from:date:message-id:subject:to:content-type; b=EZQ2zTHxQQsehYae/2qkBRNl7GRuo7QsHa7E8lptI8ZLcprPtM/dqBEqe1OmQB6Pc2 7TMTAXZMdTkWtwC5lySy19tskj6KJ/sECft5BKplzBuhXHijzlzHglvh/y8RRUP/T+f8 mrirLfF41Bjd7Bzj++TjXL9SFHRXdlZ+3y1es=
Hi,
The following does not work as expected:
Parameter f : Type -> Type.
Notation s := (f Type).
Check s.
Indeed the result is
f Type
: Type
instead of
s
: Type
I guess the reason is that "Type" is polymorphic, and is never considered to be the same as itself (my example works if you replace "f Type" by "f Set").
Is there a way to make Coq display the notation "s"?
I do not want to use explicit universes ("Definition U := Type"), because I would then need to keep track by hand of the levels to avoid universe inconsistencies.
I tried to make the argument of "f" implicit, but this does not work.
Thanks,
Guillaume
- [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.