Exploring the prelude

Stream: lean4

[David Thrane Christiansen]

When I want to know what's in the Prelude, I use some combination of go-to-definition and ripgrep. This works, but it's annoying and it's hard to recommend to others.

Is there a better way?

For instance, Coq has its various Search commands. Idris 1 had an :apropos command at the REPL that, in the environment, searches names, the names that occur in their types, and docstrings for things that contain a given string. :search finds definitions with types that are roughly isomorphic to a given type, similarly to Hoogle in Haskell.

[Kyle Miller]

The mathlib4 documentation can be helpful, especially since it shows everything with nice notation even if that notation is defined later (just ignore the Mathlib section and focus on Init): https://leanprover-community.github.io/mathlib4_docs/

[David Thrane Christiansen]

Thanks for that! Is there a ready way to locally generate something this for only the things that ship with Lean? This is for programming-focused beginners.

[Gabriel Ebner]

Another good trick is to use the workspace symbol search (ctrl-p # in vscode).

[Henrik Böving]

@David Thrane Christiansen yes, it is generated with https://github.com/leanprover/doc-gen4 you could run it against an empty lake project and it will output docs for Init, Std and Lean

[David Thrane Christiansen]

@Gabriel Ebner in my case, it seems to be called M-x consult-lsp-symbols. It searches names, which is very useful, but doesn't seem to search type signatures nor docs. Still, it's much better than nothing - thanks!

[David Thrane Christiansen]

@Henrik Böving Thanks!

[Henrik Böving]

David Thrane Christiansen said:

Gabriel Ebner in my case, it seems to be called M-x consult-lsp-symbols. It searches names, which is very useful, but doesn't seem to search type signatures nor docs. Still, it's much better than nothing - thanks!

Oh and type search is on my list for doc-gen some time in the future :tm: You could use mathlibs #find right now though.

[Sebastian Ullrich]

The LSP workspace symbols request sadly is severely lacking. Both the lack of server-side sorting (could also be blamed on the VS Code client undoing it) and of any kind of labels for e.g. displaying types (not that we could include them in the search without some hefty optimizations) are such baffling omissions.

[David Thrane Christiansen]

It's certainly better than nothing!

[Sebastian Ullrich]

Oh yeah, I'm definitely glad with what we have! You could even write a bachelor's thesis about it! https://pp.ipd.kit.edu/publication.php?id=mennicken22bachelorarbeit