def Lake.mkRelPathString (path : Lake.FilePath) : String

Convert a relative file path to a platform-independent string. Uses / as the path separator, even on Windows.

Equations

• Lake.mkRelPathString path = if System.Platform.isWindows = true then String.map (fun (c : Char) => if c = '\\' then '/' else c) path.toString else path.toString

def Lake.instToJsonFilePath_lake : Lean.ToJson Lake.FilePath

Equations

• Lake.instToJsonFilePath_lake = { toJson := fun (path : Lake.FilePath) => Lean.toJson (Lake.mkRelPathString path) }

def Lake.instToExprFilePath_lake : Lean.ToExpr Lake.FilePath

Equations

• Lake.instToExprFilePath_lake = { toExpr := fun (p : Lake.FilePath) => Lean.mkApp (Lean.mkConst `System.FilePath.mk) (Lean.toExpr p.toString), toTypeExpr := Lean.mkConst `System.FilePath }