Zulip Chat Archive
Stream: new members
Topic: Trig Functions
ROCKY KAMEN-RUBIO (May 27 2020 at 14:56):
Where do trig functions live in mathlib? I've found some old threads talking about them getting added but haven't been able to find them after a quick search.
Bryan Gin-ge Chen (May 27 2020 at 14:57):
https://leanprover-community.github.io/mathlib_docs/analysis/special_functions/trigonometric.html
Kevin Buzzard (May 27 2020 at 14:57):
search for sin
Kevin Buzzard (May 27 2020 at 14:58):
(in VS code with a project open which has mathlib as a dependency, and make sure the VS Code option for searching dependencies is switched on)
ROCKY KAMEN-RUBIO (May 27 2020 at 15:11):
Kevin Buzzard said:
(in VS code with a project open which has mathlib as a dependency, and make sure the VS Code option for searching dependencies is switched on)
How do I turn on the search dependency option? I had tried this but just got a 'no definition found for sin' message.
Kevin Buzzard (May 27 2020 at 15:13):
Kevin Buzzard (May 27 2020 at 15:14):
You want to make sure that cog isn't light blue; this is a common problem at Xena, because unfortunately the default value is not to search dependencies and so basically search works for no newcomer
Kevin Buzzard (May 27 2020 at 15:14):
You might have to reveal the cog by clicking on some ... or what have you
Kevin Buzzard (May 27 2020 at 15:15):
Every time you start a new project you have to switch it off
ROCKY KAMEN-RUBIO (May 27 2020 at 15:29):
Screen-Shot-2020-05-27-at-11.27.52-AM.png
You're talking about this window? I'm not seeing an option to change search dependencies.
Kevin Buzzard (May 27 2020 at 15:30):
No, I'm talking about what you get when you click the magnifying glass
Shing Tak Lam (May 27 2020 at 15:30):
Kevin Buzzard said:
Every time you start a new project you have to switch it off
There's a Global Setting Search: Use Ignore Files, if you always want the search to search for everything, and don't use the .gitignore files.
Last updated: Dec 20 2023 at 11:08 UTC