find all lean files recursively

Stream: lean4

[Arthur Paulino]

I've written the following function to find all lean files in a directory:

partial def getFilePathsList (fp : FilePath) (acc : List FilePath := []) :
IO (List FilePath) := do
  if ← fp.isDir then
    let mut extra : List FilePath ← []
    for dirEntry in (← fp.readDir) do
      for innerFp in ← getFilePathsList dirEntry.path do
        extra ← extra.concat innerFp
    acc ++ extra
  else
    if (getFilePathExtension fp) = "lean" then
      acc.concat fp
    else
      acc

Is there something I can use out-of-the-box though?