is Lean filename agnostic

Stream: general

[Eric Rodriguez]

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]

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

[Eric Wieser]

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

[Eric Rodriguez]

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

[Eric Wieser]

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]

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