Stream: new members
Topic: search mathlib in vscode
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?
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