names of imported files

Stream: general

[Kevin Buzzard]

Someone opened an issue in the complex number game, asking me to rename files like in Patrick's tutorial project. So I renamed basic.lean to 00-basic.lean and then I found that I couldn't import it any more (I could open it, I just couldn't import it). Is this expected behaviour? I renamed it level-00-basic.lean but still it didn't seem to work. Is this also expected behaviour? Unlike the tutorial project, I need to import previous files to make later files work. Is there any way of indicating which order they should be tackled in, or should I have unnumbered files, and then numbered files for the exercises, which are copies, and which import the unnumbered files?

[Johan Commelin]

Weird... vector2 doesn't give issues..

[Kevin Buzzard]

got it, it's the - signs. Level_00_basic can be imported, but not 00_basic or Level-00-basic

[Kevin Buzzard]

so currently my model is "can't begin with a digit, and can't have - anywhere in the filename". How close am I?

[Patrick Massot]

In the tutorial I don't import those files whose name start with digits.

[Patrick Massot]

You can still import them by putting their names between French quotes

[Keeley Hoek]

It's probably the same condition as any other name in lean being a valid identifier in any context