Hi everyone. I haven't used Coq in a long time and now I'm trying to remember how to find theorems already proved either in the standard library, any loaded library or by myself. I see in Proof General the Find Theorems command (`C-c C-f`

) but I don't know what to write there to get any theorems. I also vaguely remember one could use Search or something like that to find theorems by their type. I hope someone can help me remember here and point me to some documentation.

I found it! Page 203 of Coq's reference manual for version 8.15.0.

Ricardo has marked this topic as resolved.

Last updated: Jan 31 2023 at 14:03 UTC