Zulip Chat Archive

Stream: new members

Topic: search mathlib in vscode

view this post on Zulip Chris M (Aug 16 2020 at 03:53):

Is there an easy way to search the entire contents of mathlib within VSCode, in the panel on the left where the entire contents are shown?

view this post on Zulip Alex J. Best (Aug 16 2020 at 04:15):

If you click the three dots to the bottom right of the search box, two boxes open, files to include and files to exclude, on the right of the files to exclude is a little cog icon, it should be deselected to search all of mathlib

Last updated: May 16 2021 at 05:21 UTC