Searching in the codebase?

Stream: lean4

[Vladimir Marko]

I just installed Lean4, so newbie questions:
I notice that ℕ is not defined by default (unknown identifier 'ℕ'), while Nat is.

1. What do I need to import to get ℕ as an alias for Nat?
2. How do I go in general about searching for stuff in the libraries? Is there some kind of "Hoogle" equivalent? Can I access it or some other useful search feature from the VSCode plugin?

[Henrik Böving]

1. You could use mathlib4 which probably defines this notation or define it yourself with notation "ℕ" => Nat but there is no built in for it at the moment
2. There is currently some work on documentation (And documentation exploration) tooling but its still in very very early stages, I usually use a mix of looking at the auto completion suggestions + grepping in the lean4 repository but I don't know whether there is a better way right now, there very well might be.

[Mac]

@Vladimir Marko Lean 4 is very much still in its early stages, so there is not much tooling yet. If you want that level of support, it is best to stick with Lean 3 for now. As @Henrik Böving ,you can add mathlib4 as a dependency if you want to get the ℕ notation. Note, though, that mathlib4 is not a complete port of mathlib yet, so it will be missing out on a lot theorems / tactics / etc. that you may want.

[Scott Morrison]

Once you have mathlib4, you can import Mathlib.Tactic.LibrarySearch and use librarySearch as a helper for finding things. As Mac said, however, the mathematics library has not been ported to Lean 4 yet, so there's not much to find!