Getting an array of all file paths in PhysLean.

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 PhysLean.

Equations

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

def allPhysLeanModules : IO (Array Lean.Name)

Gets an array of all module names in PhysLean.

Equations

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