leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: new members

Topic: library search


Dean Young (Dec 26 2022 at 01:30):

Could someone remind me of the necessary import for library search in Lean 4?

David Renshaw (Dec 26 2022 at 01:31):

import Mathlib.Tactic.LibrarySearch

Kevin Buzzard (Dec 26 2022 at 08:44):

With questions like this I just usually fire up mathlib and search the repo for LibrarySearch because the Mathlib.lean file has a huge list of imports


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll