Zulip Chat Archive

Stream: general

Topic: is Lean filename agnostic

Eric Rodriguez (Sep 14 2021 at 10:04):

I currently compile some files by moving them over to temp files. This obviously changes the filename, so I'm wondering, if I have a file named myamazingfile123.lean, does Lean care about the specific filename? So for example, something like:

import data.finset.basic

def finset := (1 : )

example : (1 : ) = (myamazingfile123.finset) := rfl

Eric Rodriguez (Sep 14 2021 at 10:04):

(this is possible in Coq in some ways, so would be nice to avoid the pathologies here)

Eric Wieser (Sep 14 2021 at 10:24):

What do you mean by myamazingfile123.finset? Namespaces and filenames are unrelated in lean

Eric Rodriguez (Sep 14 2021 at 10:25):

I meant basically does some syntax like that exist at all? or are filenames irrelevant within the file

Eric Wieser (Sep 14 2021 at 10:27):

I think your question is equivalent to "is there a meta command that gets the current filename"? Since if the answer to that is yes, arbitrary code can be generated at import.

Sebastien Gouezel (Sep 14 2021 at 10:34):

A pragmatic answer is that everything is filename agnostic. Use namespaces instead.

Last updated: Aug 03 2023 at 10:10 UTC