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