coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Same symbol for functions and implication

From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
To: AUGER Cédric <sedrikov AT gmail.com>
Cc: "N. Raghavendra" <raghu AT hri.res.in>, Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Same symbol for functions and implication
Date: Mon, 9 Sep 2013 10:03:18 +0200

I do not remember if starting the session with "-nois" parameter
triggers an error when you write "A -> B".

The arrow is a built-in syntax rule in v8.4 and before (hence it still works with -nois). In the current trunk, however, it is a notation (defined in Logic.v). So coqtop -nois doesn't know of the arrow.

[Coq-Club] Same symbol for functions and implication, N. Raghavendra, 09/08/2013
- Re: [Coq-Club] Same symbol for functions and implication, Guillaume Brunerie, 09/08/2013
  - [Coq-Club] Re: Same symbol for functions and implication, N. Raghavendra, 09/09/2013
- Re: [Coq-Club] Same symbol for functions and implication, Daniel de Rauglaudre, 09/08/2013
- Re: [Coq-Club] Same symbol for functions and implication, AUGER Cédric, 09/08/2013
  - Re: [Coq-Club] Same symbol for functions and implication, Arnaud Spiwack, 09/09/2013