The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Wed, 8 Jun 2011 17:03:57 +0200,
Guillaume Brunerie 
<guillaume.brunerie AT gmail.com>
 a écrit :

> 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

You can use:

Notation "'s'" := (f _).

It should work, but you will also have "s" printed for "f nat" for
instance.

I guess it is not possible to do exactly what you want, as notations
have to be matched against holes or partly defined terms and type is
not matchable as far as I understand.

I tried:
Notation "'t'" := (f (Type: _)).

but it doesn't work better.

But