Zulip Chat Archive

Stream: general

Topic: names of imported files

Kevin Buzzard (May 28 2020 at 12:19):

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 (May 28 2020 at 12:20):

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

Kevin Buzzard (May 28 2020 at 12:22):

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

Kevin Buzzard (May 28 2020 at 12:23):

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 (May 28 2020 at 12:34):

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

Patrick Massot (May 28 2020 at 12:34):

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

Keeley Hoek (May 29 2020 at 04:06):

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

Last updated: Dec 20 2023 at 11:08 UTC