Digits in Project Name

Stream: lean4

[Filippo A. E. Nuccio]

I am giving a talk next week and I created a new project called 04Sep24 and everything seemed to work fine until I decided to create a file myfile.lean and import it. The line

import 04Sep24.myfile

seems to create problems (unexpected token; expected identifier). Is there a way out (importing only myfile does not work and I do not know how to tell " it is in your very same directory") or is it a known issue that project names should not contain/begin with digits?

[Damiano Testa]

Does using \f<<>> help?

[Kevin Buzzard]

I think that beginning with a digit is the problem, and you can probably quote your way around it if you can remember how to do the double french quotes

[Filippo A. E. Nuccio]

Let me try

[Kevin Buzzard]

Fortunately Damiano just reminded us

[Damiano Testa]

(And yes, identifiers cannot start with a digit and the guillemets should be a workaround.)

[Filippo A. E. Nuccio]

Great, thanks! It worked, I guess the \f has something to do with "French", right?

[Damiano Testa]

I think so...

[Damiano Testa]

I can trace the f for French in \f<> to this section of #tpil. I imagine that \f<<>> has the same origin.