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?


1 Answer 1


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!


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.