how to import additional theorems and notation available in

Stream: new members

[AnduinHS]

I don't know how to import additional theorems and notation available in auxiliary library by loading with the command import data. as in the following figure. I have followed "Installing Lean and mathlib on Windows"(https://leanprover-community.github.io/install/windows.html). The symobol ᶜ for complementation does not work as well. What should I do? Thank you in advance! 360截图184307077911387.png

[Eric Wieser]

Your import problem is real, but the syntax for ᶜ is Aᶜ not ᶜA

[Scott Morrison]

Have you opened a folder (not just a single file)? Does that folder have a leanpkg.toml file in the root directory, with your .lean file under src/?

[Scott Morrison]

Have you also read https://leanprover-community.github.io/install/project.html?

[Kevin Buzzard]

Yes, you can't import mathlib files with a standalone file, it needs to be part of a project which has mathlib as a dependency, for example a project made with leanproject new

[AnduinHS]

I have tried to following this. However, after I created my project in the

lib

file , my lean in VS-Code became like this:
360截图18750813536580.png .
What should I do?
I then removed my project folder to Desktop.

[Eric Wieser]

Can you paste the log message from the "Output" pane?

[Shing Tak Lam]

AnduinHS said:

I have tried to following this. However, after I created my project in the

lib

file , my lean in VS-Code became like this:
360截图18750813536580.png .
What should I do?
I then removed my project folder to Desktop.

I'm guessing from the name of the screenshots and the error you're getting, but are you in China? That might be causing the issues that you're seeing.

[Kevin Buzzard]

right -- the error seems to say "you cannot access github.com".

[AnduinHS]

Yes.
Being busy with couples of days, I have tried again to follow the instrction.
And I don't gain the expected results. It seems that the problem is in my version.
1233222.PNG 1233444.PNG

[Eric Wieser]

Now it looks like your version of git is too old

[Eric Wieser]

Or perhaps your version of python

[Eric Wieser]

It's also possible something is trying to man-in-the-middle your HTTPS requests, either a local tool as described here or possibly something more malicious.