Stream: Coq users

Topic: Searching the standard library


view this post on Zulip Bolton Bailey (Jun 05 2022 at 18:09):

Hey I am wanting to use the fact that for natural numbers, 0 = a - b <-> a <= b. Is this in the standard library somewhere?

Incidentally, what's the best way to search for a lemma like this? The ideal for me would be some kind of search bar where I can type in "nat sub eq zero iff le" and potentially get a result. There's this index but this requires you to input the first letter of the declaration you want, and is not really searchable.

view this post on Zulip Li-yao (Jun 05 2022 at 18:12):

Search Nat.sub O eq iff.

view this post on Zulip Ana de Almeida Borges (Jun 05 2022 at 18:50):

Search is very powerful but also very literal, so it can take some skill to use well. See the examples in the refman for inspiration.

view this post on Zulip Ana de Almeida Borges (Jun 05 2022 at 18:53):

Some advice from my experience: if you're looking for a lemma that should exist but can't find it, try widening your net, by either removing search terms or being less specific. For example, Search (0 = _ - _) is more specific than Search 0 (_ - _).


Last updated: Feb 06 2023 at 13:03 UTC