如何拼接文件路径🔗

要拼接文件路径，可以使用 System.FilePath 模块。你可以用 System.mkFilePath 创建一个文件路径，然后用 / 运算符把它与另一个路径拼接起来：

def concatPaths (base : System.FilePath) (sub : String)
  : System.FilePath := base / System.mkFilePath [sub]

{ toString := "home/user/dir" }#eval concatPaths (System.mkFilePath ["home", "user"]) "dir"
{ toString := "home/user/dir" }#eval System.mkFilePath ["home", "user"] 
  / System.mkFilePath ["dir"]

这个对象你可以像平常一样使用，因为新路径仍然是一个 System.FilePath 对象。