import local file

Stream: lean4

[Elisabeth Bonnevier]

How do I import one local file into another file in the same folder? I have not been able to find documentation on how to work with modules in Lean 4.

[Horațiu Cheval]

Do the examples in the Lake repository help?

[Sebastian Ullrich]

Relevent FPiL section: https://leanprover.github.io/functional_programming_in_lean/hello-world/starting-a-project.html

[Elisabeth Bonnevier]

Sebastian Ullrich said:

Relevent FPiL section: https://leanprover.github.io/functional_programming_in_lean/hello-world/starting-a-project.html

I got it to work. Thanks!