coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] curious behavior of "Locate" command

From: Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] curious behavior of "Locate" command
Date: Wed, 8 Jun 2016 15:07:13 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=5764c029b688c1c0d24a2e97cd764f AT gmail.com; spf=Pass smtp.mailfrom=5764c029b688c1c0d24a2e97cd764f AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f53.google.com
Ironport-phdr: 9a23:a5OJJhAutimrACltrqOqUyQJP3N1i/DPJgcQr6AfoPdwSP7+osbcNUDSrc9gkEXOFd2CrakU2qyJ6Ou9BCQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTmkb/psMCOKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46FppIZ8VvDxeL19RrhFBhwnNXo07Yvlr0rtVwyKs14VTmgU2jlPGAnGpEWnAcmtuXOg5+AjiHmRZMauQepoUG6vvvhgREC21CkvODsw8WWRgct12vEI6Cm9rgByltaHKLqeM+BzK/vQ

Dear all,

It seems that after the following commands:

Require Import BinNums.
Open Scope positive.
Require Import ZArith.

I can use the "_ ~ _" notation to construct positive integers:

Check 1~0.
Check 1~1.
Check 1~0~0.
Check 1~0~1.
Check 1~1~0.
Check 1~1~1.

However, when I try to ask Coq where is "_ ~ _" defined, I get a reply:

Unknown notation

I am not sure if I understand why Coq in this case provides the above
unhelpful message instead of indicating that it is defined in

Coq.PArith.BinPosDef

when it clearly understand that notation.

Does this behavior make sense to you or should it be considered as a bug?

Thanks in advance for the help.

[Coq-Club] curious behavior of "Locate" command, Matej Kosik, 06/08/2016
- Re: [Coq-Club] curious behavior of "Locate" command, Clément Pit--Claudel, 06/08/2016
  - Re: [Coq-Club] curious behavior of "Locate" command, Tej Chajed, 06/08/2016
    - Re: [Coq-Club] curious behavior of "Locate" command, Matej Kosik, 06/08/2016
- Re: [Coq-Club] curious behavior of "Locate" command, Guillaume Melquiond, 06/08/2016