coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT csail.mit.edu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Search vs SearchAbout
- Date: Sat, 18 May 2013 09:15:48 -0400
On 05/17/2013 09:48 PM, Math Prover wrote:
Here is my question: How does Search and SearchAbout differ in practice?
The manual states:
It is often difficult to remember the names of all lemmas and definitions
available in the current context, especially if large libraries have been
loaded. A convenient SearchAbout command is available to lookup all known
facts concerning a given predicate. For instance, if you want to know all the
known lemmas about the less or equal relation, just ask:
and
Another command Search displays only lemmas where the searched predicate
appears at the head position in the conclusion.
These explanations seem to give the complete story on the difference between the commands. Perhaps the issue is that you aren't familiar with the terminology "head position"? The upshot in this case seems to be that [Search] only considers types that match your query with extra [forall]s added in front, whereas [SearchAbout] applies a looser rule.
- [Coq-Club] Search vs SearchAbout, Math Prover, 05/18/2013
- Re: [Coq-Club] Search vs SearchAbout, Adam Chlipala, 05/18/2013
- Re: [Coq-Club] Search vs SearchAbout, Jason Gross, 05/18/2013
- Re: [Coq-Club] Search vs SearchAbout, Pierre-Marie Pédrot, 05/18/2013
- Re: [Coq-Club] Search vs SearchAbout, Jason Gross, 05/18/2013
- Re: [Coq-Club] Search vs SearchAbout, Pierre-Marie Pédrot, 05/18/2013
- Re: [Coq-Club] Search vs SearchAbout, Jason Gross, 05/18/2013
- Re: [Coq-Club] Search vs SearchAbout, Adam Chlipala, 05/18/2013
Archive powered by MHonArc 2.6.18.