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
Instances For
Equations
- Lake.instToJsonFilePath_lake = { toJson := fun (path : Lake.FilePath) => Lean.toJson (Lake.mkRelPathString path) }
Instances For
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 }