complex-number-game import

Stream: new members

[Jiekai]

The import line of src/complex/your_solutions/Level_02_I.lean is

import complex.Level_01_of_real

src/
└── complex
    ├── kb_solutions
    │   ├── Level_00_basic.lean
    │   ├── Level_01_of_real.lean
    │   ├── Level_02_I.lean
    ├── Level_00_basic.lean
    ├── Level_01_of_real.lean
    ├── Level_02_I.lean
    └── your_solutions
        ├── Level_01_of_real.lean
        ├── Level_02_I.lean

Which Level_01_of_real.lean will be imported?

[Jiekai]

I see. It's the relative path to the src/, right?

[Johan Commelin]

@Jiekai yep. You can do relative paths with import .sibling.subfile