structure System.FilePath : Type

• toString : String

instance System.instInhabitedFilePath : Inhabited System.FilePath

instance System.instDecidableEqFilePath : DecidableEq System.FilePath

Equations

• System.instDecidableEqFilePath = System.decEqFilePath✝

instance System.instHashableFilePath : Hashable System.FilePath

instance System.instReprFilePath : Repr System.FilePath

Equations

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

instance System.instToStringFilePath : ToString System.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

Equations

• System.FilePath.extSeparator = '.'

def System.FilePath.exeExtension : String

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

Equations

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

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

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

def System.FilePath.join (p sub : System.FilePath) : System.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 System.FilePath

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

Equations

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

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

Equations

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

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

Equations

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

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

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

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

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

def System.FilePath.addExtension (p : System.FilePath) (ext : String) : System.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.

def System.FilePath.withExtension (p : System.FilePath) (ext : String) : System.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

• p.withExtension ext = match p.fileStem with | none => p | some stem => p.withFileName (if ext.isEmpty = true then stem else stem ++ "." ++ ext)

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

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

Equations

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

instance System.instCoeStringFilePath : Coe String System.FilePath

Equations

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

@[reducible, inline]

abbrev System.SearchPath : Type

Equations

• System.SearchPath = List System.FilePath

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) : System.SearchPath

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

Equations

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