Zulip Chat Archive

Stream: new members

Topic: import files with spaces

Pedro Minicz (Jan 04 2022 at 22:14):

Suppose I have a Lean file with spaces on its name, say Hello World.lean, is it possible for me to import it from another file? I tried import .Hello World, import .Hello\ World and import ".Hello World", none of which worked, so I suspect it is impossible.

Reid Barton (Jan 04 2022 at 22:32):

This seems to work:

import Hello World»

but also maybe just don't do that?

Pedro Minicz (Jan 04 2022 at 22:36):


Last updated: Dec 20 2023 at 11:08 UTC