Zulip Chat Archive

Stream: new members

Topic: Trig Functions


view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (May 27 2020 at 14:57):

https://leanprover-community.github.io/mathlib_docs/analysis/special_functions/trigonometric.html

view this post on Zulip Kevin Buzzard (May 27 2020 at 14:57):

search for sin

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 27 2020 at 15:13):

cog.png

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 27 2020 at 15:14):

You might have to reveal the cog by clicking on some ... or what have you

view this post on Zulip Kevin Buzzard (May 27 2020 at 15:15):

Every time you start a new project you have to switch it off

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 27 2020 at 15:30):

No, I'm talking about what you get when you click the magnifying glass

view this post on Zulip 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: May 15 2021 at 02:11 UTC