The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I'm not sure what the exact rules are, but I think Coq treats things starting with letters and containing only alphanumerics and underscores as variables, which are bound when the notation is expanded.  Putting something in single quotes tells Coq to treat it as a symbol.  So you could do [Notation "'test' x f" := (tohfiber f x).], replacing [test] with whatever you want.

-Jason

On Fri, Feb 14, 2014 at 6:57 PM, Vladimir Voevodsky <vladimir AT ias.edu> wrote:

I do not want "test1'". As a matter of fact I do not even want "test1". I want "test".

V.

On Feb 14, 2014, at 6:38 PM, J. Ian Johnson <ianj AT ccs.neu.edu> wrote:

> Er, "'test1' x f".
> -Ian
> ----- Original Message -----
> From: "J. Ian Johnson" <ianj AT zimbra.ccs.neu.edu>
> To: coq-club AT inria.fr
> Sent: Friday, February 14, 2014 6:38:06 PM GMT -05:00 US/Canada Eastern
> Subject: Re: [Coq-Club] notations
>
> Try "'0'".
> -Ian
> ----- Original Message -----
> From: "Vladimir Voevodsky" <vladimir AT ias.edu>
> To: "coq club" <coq-club AT inria.fr>
> Sent: Friday, February 14, 2014 6:11:28 PM GMT -05:00 US/Canada Eastern
> Subject: [Coq-Club] notations
>
> Hi,
>
> why Coq does not complain at:
>
> Notation "0" := ( unel _ ) : addmonoid_scope .
>
> but says
>
> Error: A notation must include at least one symbol.
>
> at
>
> Notation "test1 x f" := ( tohfiber f x ) .
>
> ?
>
> V.