coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Resolving ambiguity between multiple notations for a single identifier
Date: Sat, 30 Apr 2016 17:09:28 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f175.google.com
Ironport-phdr: 9a23:9ho4ehfusrBo5gTvsRWTgUNhlGMj4u6mDksu8pMizoh2WeGdxc6+ZR7h7PlgxGXEQZ/co6odzbGG4+awCSdZvM/JmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbviq9uDM04R2WP1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GLdfFXEtN30/zMztrxjKCwWVtVUGVWBDsB1OChTF5ReyeprwrCb8qqIp2i6cPM77Sb05cTun5qZvDhTvjXFUZHYC7GjLh5ko3+pgqxW7qkknzg==

On 04/30/2016 03:11 PM, scott constable wrote:

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 "&&"? *)

I think that whatever scope is open and at the top of the scope stack is where your Infix "+" goes, since you didn't specify a scope for it. In that case, it probably overrides the last such notation that was in that scope (if there was one).

To recover a previous notation, you need to put the new one in a new scope:

Require Import Bool.

Definition my_b := andb true false.

Infix "+" := andb : mybscope.

Open Scope mybscope.

Print my_b.

Close Scope mybscope.

Print my_b.

-- Jonathan

[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