Def getLeanLibs

Modification history

2024-06-14 15:55

Mathlib/Util/GetAllModules.lean

chore: don't import `Lake` under `Mathlib` (#13779) …

Modified getLeanLibs View on Github →

2024-06-01 12:47

Mathlib/Util/GetAllModules.lean

refactor: tweak and move functionality for getting all modules out of `scripts` (#13339) …

Modified getLeanLibs View on Github →

2024-05-29 17:17

scripts/mk_all.lean

feat: `lake exe mk_all` as a Lean executable (#11853) …

Added getLeanLibs View on Github →