feat: add convenience coercion from String to FilePath

This commit is contained in:
Sebastian Ullrich 2021-05-27 16:29:30 +02:00
parent 619873c842
commit e4995ce8ba

View file

@ -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