The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Adam, your explanation works for trunk, where [Search] gives me things of type [Z -> Z -> bool], and [SearchAbout] gives me things of type, e.g., [Morphisms.Proper (Morphisms.respectful eq Z.eqf) Z.testbit].  But in 8.4 pl2, [Search] gives [Zneq_bool] and [Zeq_bool], and not [Z.leb], even though they are all of type [Z -> Z -> bool].  I thought it might have something to do with module scoping, but [Import Z.] does not change the result.  Perhaps this is a bug in 8.4?

-Jason

On Sat, May 18, 2013 at 9:15 AM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

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.