Def getAllFiles

Modification history

2024-06-01 12:47
Mathlib/Util/GetAllModules.lean
refactor: tweak and move functionality for getting all modules out of `scripts` (#13339) …
Added getAllFilesView on Github →