Convert a relative file path to a platform-independent string.
Uses /
as the path separator, even on Windows.
Equations
Instances For
Joins a two (potentially) relative paths.
If either path is .
, this returns the other.
Equations
Instances For
Equations
Instances For
Creates a module Name
from a file path.
The components of the path become string components of the Name
.
Before conversion, normalizes the path, removes any extensions, and
strips a trailing path separator.
Examples:
modOfFilePath "Foo/Bar" = `Foo.Bar
modOfFilePath "Foo/Bar/" = `Foo.Bar
modOfFilePath "Foo/Bar.lean" = `Foo.Bar
modOfFilePath "Foo/Bar.tar.gz" = `Foo.Bar
modOfFilePath "Foo/Bar.lean/" = `Foo.«Bar.lean»
Equations
Instances For
@[irreducible]