Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Notation with "Type"

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Notation with "Type"


chronological Thread 
  • 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



Archive powered by MhonArc 2.6.16.

Top of Page