The Coq mailing list

["J. Ian Johnson" <ianj AT ccs.neu.edu>]

The single quotes signal to Coq to treat the enclosed characters as a symbol 
rather than an identifier to match for the RHS.
'test' should do what you want.
-Ian
----- Original Message -----
From: "Vladimir Voevodsky" 
<vladimir AT ias.edu>
To: "Coq Club" 
<coq-club AT inria.fr>
Sent: Friday, February 14, 2014 6:57:47 PM GMT -05:00 US/Canada Eastern
Subject: Re: [Coq-Club] notations

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.