The Coq mailing list

[Math Prover <mathprover AT yahoo.com>]

Hi Coq-Club,

This is something that has confused me for quite a while.

Just now, I was searching for "Z.leb", since I wanted to play with integers 
rather than natural numbers.

My first attempt was to use Search, and after that failed, I tried 
SearchAbout.

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.



However, it's not clear how either explains the problem I am facing. Thanks!

=== BEGIN ===

Require Import ZArith.

Search (Z -> Z -> bool).

(*
Zneq_bool: Z -> Z -> bool
Zeq_bool: Z -> Z -> bool
*)

SearchAbout (Z -> Z -> bool).

(*
Zeq_bool: Z -> Z -> bool
Zneq_bool: Z -> Z -> bool
Z.leb: Z -> Z -> bool
.. and many more ... *)


=== END ===