Issue with Library Calls

Stream: new members

[Brandon]

Hey all, I am trying to get Lean 3 to run on my Ubuntu setup, and have gotten everything working except for imports (so I guess it's pretty generous to say that I have everything working).
Here is a screenshot of the error I receive
Screenshot-from-2023-03-10-10-03-30.png

Let me know what can be done, I'm sure its simple. Thanks!

[Alex J. Best]

did you set up a project following https://leanprover-community.github.io/install/project.html? and open the project folder in vscode?

[Brandon]

Alex J. Best said:

did you set up a project following https://leanprover-community.github.io/install/project.html? and open the project folder in vscode?

That resolved the problem! Thanks!