import local files

Stream: general

[Miguel Marco]

In lean3, i could organize my code in several files, and when i need to use the code from another file, i just needed to add the line

import .otherfile

Now that i am porting my code to lean4, it doesn't work anymore.

What is the way for doing that?

[Kevin Buzzard]

import MyProjectName.Path.To.File

[Kevin Buzzard]

will import <project root>/MyProjectName/Path/To/File.lean

[Kevin Buzzard]

You need a project name nowadays though, eg all mathlib imports now start Mathlib. whether you're working on mathlib or a dependency

[Miguel Marco]

Path starts where lakefile.leanis right?

and the project name should be the one declared in that file?

So i should put all the lean files in a subdirectory?

[Scott Morrison]

Think of that directory as replacing the src/ directory we used to use in Lean 3.