coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] notations

From: "J. Ian Johnson" <ianj AT ccs.neu.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] notations
Date: Fri, 14 Feb 2014 18:38:06 -0500 (EST)

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.

[Coq-Club] notations, Vladimir Voevodsky, 02/15/2014
- Re: [Coq-Club] notations, J. Ian Johnson, 02/15/2014
  - Re: [Coq-Club] notations, J. Ian Johnson, 02/15/2014
    - Re: [Coq-Club] notations, Vladimir Voevodsky, 02/15/2014
      - Re: [Coq-Club] notations, Jason Gross, 02/15/2014
        
        Re: [Coq-Club] notations, Vladimir Voevodsky, 02/15/2014
        
        Re: [Coq-Club] notations, Cyril Cohen, 02/15/2014
      - Re: [Coq-Club] notations, J. Ian Johnson, 02/15/2014