# How can I search only all of the lemmas in a different module (in Coq)?

I usually import QArith.

If I write

Search "max" "id".


Then I can see something like this:

Pos.max_id: forall n : positive, Pos.max n n = n
N.max_id: forall n : N, N.max n n = n
Nat.max_id: forall n : nat, Nat.max n n = n
Z.max_id: forall n : Z, Z.max n n = n


If I write

Search "Pos" "max".


Then nothing appears.

How can I search another (included?) library (or module) 's lemma?

You can use the inside keyword: Search "max" "id" inside Pos. gives you exactly one answer, Pos.max_id. If you wish to exclude a module/library, you can use the outside keyword instead. Search is a very useful command to master, and there is a lot to it, you might want to look at the full documentation to learn more about it!