coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] curious behavior of "Locate" command
Date: Wed, 8 Jun 2016 15:28:22 +0200
Authentication-results: mail3-smtp-sop.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-f51.google.com
Ironport-phdr: 9a23:Cc/ZcRYuku9iZkboZDVQk1D/LSx+4OfEezUN459isYplN5qZpcm/bnLW6fgltlLVR4KTs6sC0LqH9f+7EjJZqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7H0pMaYPVwArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5Jd2wKnxgAIA/e7RKyCsqu7Hfx7rAs0nfKbcavRug4A2irtao6FxTk13lbORY29WjWjop7i6cN80HpnAB234OBONLdD/F5ZK6IJd4=

On 06/08/2016 03:22 PM, Tej Chajed wrote:
> In this case the relevant notations are p ~ 0 and p ~ 1. The syntax for
> Locate
> <https://coq.inria.fr/refman/Reference-Manual014.html#hevea_command219>,
> while it looks similar to the patterns used in,
> for example, Search, actually only always replacing variables with _ and
> giving a complete notation, or searching for a sequence of symbols. In this
> case Locate "~". will find the two relevant notations.
>
> I think you're asking for a feature where _ can also match literals in the
> notation.
>
> On Wed, Jun 8, 2016 at 9:15 AM, Clément Pit--Claudel
> <clement.pit AT gmail.com
>
> <mailto:clement.pit AT gmail.com>>
> wrote:
>
> On 2016-06-08 09:07, Matej Kosik wrote:
> > However, when I try to ask Coq where is "_ ~ _" defined, I get a
> reply:
> >
> > Unknown notation
>
> Note that `Locate "_ ~ 0"` works.
>
>

Indeed. Its so simple. Thanks you all.

[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