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) }