how to import

Stream: new members

[Paul Chisholm]

I have two Lean modules, call then A and B, and B imports A with 'import A'. When I do this a blue wavy line appears underneath the word 'import' and the message 'configuring Test 0.1' is written to the problems area. I have also tried 'import .A' and 'import ./A' with the same result.

I am using Lean 4 nightly for 12th May and VSC Lean 4 extension v0.0.26 on MacOS.

[Yakov Pechersky]

You have to do import PackageName.A, where PackageName is the name of the folder which is also the package name in the configuration file. I think.

[Kevin Buzzard]

you'll do better off in the #lean4 stream