CoqSearch and friends?

Stream: lean4

[Siddharth Bhat]

How does one search for identifiers by name or type?

• In plain Coq, one can use the Search command to search based on identifiers, and if I recall correctly, types.
• Using proof-general in emacs, one has search functionality in the plugin to find identifiers.

What's the correct equivalent I should use in tLean ?

[Henrik Böving]

I currently use a mix of autocompletion and grep, I'm not aware of any alternative (sadly).

[Sebastian Ullrich]

We have https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Find.lean for type-directed search (and of course library_search for heavier search automation)

[Sebastian Ullrich]

Searching by name is just autocompletion, no? :)

[Tomas Skrivan]

I was curious about something similar recently. Can find and library_search list all theorems that can be used in rw on the current goal?

[Johan Commelin]

There is rw_search in mathlib. It has some performance issues, and it hasn't been ported to Lean 4.