Skip to content

Narrow the two bare import Mathlib to the modules actually used - #40

Merged
leonardoalt merged 1 commit into
mainfrom
narrow-mathlib-imports
Jul 29, 2026
Merged

Narrow the two bare import Mathlib to the modules actually used#40
leonardoalt merged 1 commit into
mainfrom
narrow-mathlib-imports

Narrow the two bare `import Mathlib` to the modules actually used

a06f970
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

Annotations

1 warning
Build & check
succeeded Jul 29, 2026 in 2m 13s