coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] notations

From: Vladimir Voevodsky <vladimir AT ias.edu>
To: coq club <coq-club AT inria.fr>
Subject: [Coq-Club] notations
Date: Fri, 14 Feb 2014 18:11:28 -0500

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