Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Search vs SearchAbout

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Search vs SearchAbout


Chronological Thread 
  • 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.



Archive powered by MHonArc 2.6.18.

Top of Page