Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.
Sign up to join this community
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!
