structure System.FilePath : Type

• toString : String

instance System.instInhabitedFilePath : Inhabited Lake.FilePath

instance System.instDecidableEqFilePath : DecidableEq Lake.FilePath

instance System.instHashableFilePath : Hashable Lake.FilePath

instance System.instReprFilePath : Repr Lake.FilePath

instance System.instToStringFilePath : ToString Lake.FilePath

def System.FilePath.pathSeparator : Char

The character that separates directories. In the case where more than one character is possible, pathSeparator is the 'ideal' one.

def System.FilePath.pathSeparators : List Char

The list of all possible separators.

def System.FilePath.extSeparator : Char

File extension character

def System.FilePath.exeExtension : String

def System.FilePath.normalize (p : Lake.FilePath) : Lake.FilePath

def System.FilePath.isAbsolute (p : Lake.FilePath) : Bool

def System.FilePath.isRelative (p : Lake.FilePath) : Bool

def System.FilePath.join (p : Lake.FilePath) (sub : Lake.FilePath) : Lake.FilePath

instance System.FilePath.instDivFilePath : Div Lake.FilePath

instance System.FilePath.instHDivFilePathString : HDiv Lake.FilePath String Lake.FilePath

def System.FilePath.parent (p : Lake.FilePath) : Option Lake.FilePath

def System.FilePath.fileName (p : Lake.FilePath) : Option String

def System.FilePath.fileStem (p : Lake.FilePath) : Option String

Extracts the stem (non-extension) part of p.fileName.

def System.FilePath.extension (p : Lake.FilePath) : Option String

def System.FilePath.withFileName (p : Lake.FilePath) (fname : String) : Lake.FilePath

def System.FilePath.withExtension (p : Lake.FilePath) (ext : String) : Lake.FilePath

def System.FilePath.components (p : Lake.FilePath) : List String

def System.mkFilePath (parts : List String) : Lake.FilePath

instance System.instCoeStringFilePath : Coe String Lake.FilePath

@[inline, reducible]

abbrev System.SearchPath : Type

def System.SearchPath.separator : Char

The character that is used to separate the entries in the $PATH (or %PATH%) environment variable.

def System.SearchPath.parse (s : String) : Lake.SearchPath

def System.SearchPath.toString (path : Lake.SearchPath) : String