structure System.FilePath : Type

• toString : String

Instances For

• Lake.instCheckExistsFilePath
• Lake.instCoeFilePathGitRepo
• Lake.instCoeTextFilePathFilePath
• Lake.instComputeHashFilePathIO
• Lake.instGetMTimeFilePath
• Lean.instFromJsonFilePath
• Lean.instToExprFilePath
• Lean.instToJsonFilePath
• System.FilePath.instDiv
• System.FilePath.instHDivString
• System.instCoeStringFilePath
• System.instHashableFilePath
• System.instInhabitedFilePath
• System.instReprFilePath
• System.instToStringFilePath

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

• p.isAbsolute = (System.FilePath.pathSeparators.contains p.toString.front || System.Platform.isWindows && decide (p.toString.length > 1) && p.toString.iter.next.curr == ':')

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

Equations

• p.isRelative = !p.isAbsolute

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

Equations

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

instance System.FilePath.instDiv : Div Lake.FilePath

Equations

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

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

Equations

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

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

Equations

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

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

• p.withFileName fname = match p.parent 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

• p.addExtension ext = match p.fileName with | none => p | some fname => p.withFileName (if ext.isEmpty = true then fname else fname ++ "." ++ ext)

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.

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

Equations

• p.components = p.normalize.toString.splitOn System.FilePath.pathSeparator.toString

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

Equations

• System.mkFilePath parts = { toString := System.FilePath.pathSeparator.toString.intercalate parts }

instance System.instCoeStringFilePath : Coe String Lake.FilePath

Equations

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

@[reducible, inline]

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 (s.split fun (c : Char) => System.SearchPath.separator == c)

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

Equations

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