Getting an array of all file paths in Physlib.

partial def allFilePaths.go (prev : Array System.FilePath) (root : String) (path : System.FilePath) : IO (Array System.FilePath)

The recursive function underlying allFilePaths.

def allFilePaths : IO (Array System.FilePath)

Gets an array of all file paths in Physlib.

Equations

• allFilePaths = allFilePaths.go #[] "./Physlib" { toString := "./Physlib" }

def allPhyslibModules : IO (Array Lean.Name)

Gets an array of all module names in Physlib.

Equations

• One or more equations did not get rendered due to their size.