Zulip Chat Archive

Stream: general

Topic: names of imported files


view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 28 2020 at 12:20):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (May 28 2020 at 12:34):

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

view this post on Zulip Patrick Massot (May 28 2020 at 12:34):

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

view this post on Zulip 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: May 15 2021 at 23:13 UTC