Commit 2023-08-29 02:16 b9d6ccb6

View on Github →

chore: reduce withImportModules duplication (#6482)

Estimated changes

Modified ImportGraph/Main.lean

Modified Mathlib.lean

Created Mathlib/Lean/CoreM.lean

added def CoreM.withImportModules

Modified lake-manifest.json

Modified scripts/checkYaml.lean

Modified scripts/runLinter.lean