coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Tej Chajed <tchajed AT mit.edu>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] curious behavior of "Locate" command
Date: Wed, 8 Jun 2016 09:22:43 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tchajed AT mit.edu; spf=Pass smtp.mailfrom=tchajed AT mit.edu; spf=None smtp.helo=postmaster AT dmz-mailsec-scanner-4.mit.edu
Ironport-phdr: 9a23:XfZHRxPlpvQJxTmAVsAl6mtUPXoX/o7sNwtQ0KIMzox0KPj7rarrMEGX3/hxlliBBdydsKIVzbWN+P29EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35XxiLv5psCbSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6Lpyv/JHBK79ZuEzSaFSRGAtNHlw78n2vzHCSxGO7z0SSDNFvABPBl354ROydZf4sCb2/r5h0ymTP8D6ZbU1RXKv47o9G0ygszsOKzNsqDKfscd3lq8O+B8=

In this case the relevant notations are p ~ 0 and p ~ 1. The syntax for Locate, 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> 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.

[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