coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Resolving ambiguity between multiple notations for a single identifier

From: scott constable <sdconsta AT syr.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Resolving ambiguity between multiple notations for a single identifier
Date: Sat, 30 Apr 2016 15:11:31 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=sdconsta AT syr.edu; spf=None smtp.mailfrom=sdconsta AT syr.edu; spf=None smtp.helo=postmaster AT smtp1.syr.edu
Ironport-phdr: 9a23:SHjHGxV2p6a7cTukx4dU1Sl7JSnV8LGtZVwlr6E/grcLSJyIuqrYZheAt8tkgFKBZ4jH8fUM07OQ6PCwHzxQqs/b7zgrS99laVwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oM2DJVUYz2PnPvtbF1afk0b4joEum4xsK6I8mFPig0BjXKBo/15uPk+ZhB3m5829r9ZJ+iVUvO89pYYbCf2pN/dwcbsNBzM/dmsx+cfDtB/ZTALJ6GFPfH8Rl09TCA/Z8FnxWZHqriLwsuc1jDKWNsrwVqw9cS+z9eFmRAK+23RPDCIw7GyC0p84t6lcuh/0/xE=

Hi All,

The reference manual gives a terrific explanation of how Coq resolves ambiguity in the mapping from notation to identifier via the scope stack. However, I can't seem to find an explanation on how Coq resolves ambiguity in the mapping from identifier to notation when displaying symbolic notations (one might expect such an explanation in Section 12.1.5 of the manual). For instance,

Require Import Bool.

Definition my_b := andb true false.

Infix "+" := andb.

Print my_b.

(* At this point, andb has two notations: "+" and "&&". How does Coq choose which to display? Once I have defined the "+" notation, can I go back to using "&&"? *)

Thanks in advance,

~Scott Constable

[Coq-Club] Resolving ambiguity between multiple notations for a single identifier, scott constable, 04/30/2016
- Re: [Coq-Club] Resolving ambiguity between multiple notations for a single identifier, Jonathan Leivent, 04/30/2016