The Coq mailing list

[Guillaume Brunerie <guillaume.brunerie AT gmail.com>]

2011/6/8 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 :

> Is there a way to make Coq display the notation "s"?

You can use:

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

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

This is not exactly what I want, I want to use "s" as a shortcut for the term "f Type", in particular I want also be able to use "s" instead of "f Type".
"f" is a function is some other file, but in the proofs I’m writing I only need "f Type" (I will never apply "f" to "nat") and I want a shortcut for that (because it is actually much longer than "f Type", there are three other arguments which will never change too)

Anyway, I found a solution while reading your message :

Definition temporary_name := f Type.
Notation "s" := temporary_name.

And then I can use "s" anywhere, and "s" is printed by coq (and I have no universe inconsistency so far).

Thanks :)


Guillaume