diff --git a/src/Init/System/FilePath.lean b/src/Init/System/FilePath.lean index 4bdae56b71..343506e199 100644 --- a/src/Init/System/FilePath.lean +++ b/src/Init/System/FilePath.lean @@ -114,6 +114,9 @@ end FilePath def mkFilePath (parts : List String) : FilePath := ⟨String.intercalate FilePath.pathSeparator.toString parts⟩ +instance : Coe String FilePath where + coe := FilePath.mk + abbrev SearchPath := List FilePath namespace SearchPath