structure System.FilePath : Type

• toString : String

instance System.instInhabitedFilePath : Inhabited Lake.FilePath

Equations

• System.instInhabitedFilePath = { default := { toString := default } }

instance System.instDecidableEqFilePath : DecidableEq Lake.FilePath

Equations

• System.instDecidableEqFilePath = System.decEqFilePath✝

instance System.instHashableFilePath : Hashable Lake.FilePath

Equations

• System.instHashableFilePath = { hash := System.hashFilePath✝ }

instance System.instReprFilePath : Repr Lake.FilePath

Equations

• System.instReprFilePath = { reprPrec := fun (p : Lake.FilePath) => Repr.addAppParen (Std.Format.text "FilePath.mk " ++ repr p.toString) }

instance System.instToStringFilePath : ToString Lake.FilePath

Equations

• System.instToStringFilePath = { toString := fun (p : Lake.FilePath) => p.toString }

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.

Equations

• System.FilePath.pathSeparator = if System.Platform.isWindows = true then '\\' else '/'

def System.FilePath.pathSeparators : List Char

The list of all possible separators.

Equations

• System.FilePath.pathSeparators = if System.Platform.isWindows = true then ['\\', '/'] else ['/']

def System.FilePath.extSeparator : Char

File extension character

Equations

• System.FilePath.extSeparator = '.'

def System.FilePath.exeExtension : String

Equations

• System.FilePath.exeExtension = if System.Platform.isWindows = true then "exe" else ""

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• System.FilePath.isRelative p = !System.FilePath.isAbsolute p

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

Equations

• System.FilePath.join p sub = if System.FilePath.isAbsolute sub = true then sub else { toString := p.toString ++ Char.toString System.FilePath.pathSeparator ++ sub.toString }

instance System.FilePath.instDivFilePath : Div Lake.FilePath

Equations

• System.FilePath.instDivFilePath = { div := System.FilePath.join }

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

Equations

• System.FilePath.instHDivFilePathString = { hDiv := fun (p : Lake.FilePath) (sub : String) => System.FilePath.join p { toString := sub } }

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

Equations

• System.FilePath.parent p = System.FilePath.mk <$> String.extract p.toString { byteIdx := 0 } <$> System.FilePath.posOfLastSep p

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• System.FilePath.withFileName p fname = match System.FilePath.parent p with | none => { toString := fname } | some p => p / fname

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

Appends the extension ext to a path p.

ext should not contain a leading ., as this function adds one. If ext is the empty string, no . is added.

Unlike System.FilePath.withExtension, this does not remove any existing extension.

Equations

• One or more equations did not get rendered due to their size.

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

Replace the current extension in a path p with ext.

ext should not contain a ., as this function adds one. If ext is the empty string, no . is added.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• System.FilePath.components p = String.splitOn (System.FilePath.normalize p).toString (Char.toString System.FilePath.pathSeparator)

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

Equations

• System.mkFilePath parts = { toString := String.intercalate (Char.toString System.FilePath.pathSeparator) parts }

instance System.instCoeStringFilePath : Coe String Lake.FilePath

Equations

• System.instCoeStringFilePath = { coe := System.FilePath.mk }

@[inline, reducible]

abbrev System.SearchPath : Type

Equations

• Lake.SearchPath = List Lake.FilePath

def System.SearchPath.separator : Char

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

Equations

• System.SearchPath.separator = if System.Platform.isWindows = true then ';' else ':'

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

Equations

• System.SearchPath.parse s = List.map System.FilePath.mk (String.split s fun (c : Char) => System.SearchPath.separator == c)

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

Equations

• System.SearchPath.toString path = String.intercalate (Char.toString System.SearchPath.separator) (List.map System.FilePath.toString path)