Can someone help me to solve this problem in VSCode

Stream: new members

[Kyle Yank]

image.png

[Kyle Yank]

I don't know how to download the package

[Riccardo Brasca]

Have you opened the folder of the project rather than the single file?

[Kyle Yank]

Where's the folder?

[Riccardo Brasca]

You are working on mathlib, right? I mean the mathlib folder where the file you opened is located

[Kyle Yank]

yep

[Kyle Yank]

And then,what should I do

[Riccardo Brasca]

In vs code you need to select "open folder" and open the mathlib4 folder

[Kyle Yank]

If I don't have mathlib4 ,then what should Ido

[Riccardo Brasca]

How did you get the file you have already opened?

[Kyle Yank]

in mathlib

[Riccardo Brasca]

So you have mathlib

[Kyle Yank]

I opened a new text file, and just pasted the code from mathlib

[Kyle Yank]

Should I download the mathlib4 folder in my computer?

[Riccardo Brasca]

I see.

git clone https://github.com/leanprover-community/mathlib4.git
cd mathlib4
lake exe cache get

Will download for you everything you need to work with mathlib.

[Riccardo Brasca]

You can also do it via the vs code interface, click on the \forall symbol, then download project or something similar (I am on mobile)

[Kyle Yank]

I actually still do not understand what you told me to do

[Kyle Yank]

Where is the \forall symbol

[Kyle Yank]

You mean,I paste this in the git CMD?

[Kyle Yank]

image.png

[Martin Dvořák]

I think this icon (in VS Code, assuming you have the right plugin) was meant:
image.png

[Kyle Yank]

image.png

[Dan Velleman]

@Kyle Yank : Have you read this: https://leanprover-community.github.io/install/project.html?

[Kyle Yank]

I’m gonna check it right now.