Zulip Chat Archive

Stream: new members

Topic: import troubles?

Kristaps Balodis (Jul 06 2022 at 05:29):

Hi!
Haven't touched Lean for a while, just downloaded Lean4 in VS Code, everything seems to work fine, except when I try to import anything I get this error message:

untitled:Untitled-1:2:0

What do?

Arthur Paulino (Jul 06 2022 at 10:32):

Are you inside a Lake project? What's the output of lake build?

Last updated: Dec 20 2023 at 11:08 UTC