Zulip Chat Archive

Stream: lean4

Topic: Searching in the codebase?


Vladimir Marko (Nov 15 2021 at 13:51):

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 (Nov 15 2021 at 13:57):

  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 (Nov 15 2021 at 16:20):

@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 (Nov 15 2021 at 21:14):

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!


Last updated: Dec 20 2023 at 11:08 UTC