Commit 02052d4
chore: bump mathlib to 6cf3ab1, fix breaking changes (#547)
Bump `mathlib` dependency to
[6cf3ab1](leanprover-community/mathlib4@6cf3ab1):
chore: make argument in `zero_le`/`one_le` implicit (#38148)
(2026-04-29)
Previously at:
[6727686](leanprover-community/mathlib4@6727686):
ci(olean_report): use `lake env` instead of `lake exec` to invoke cache
binary (#38712) (2026-04-29)
Tracking issue: #546
---
This PR bumps `mathlib` to an identified incompatible (first-known-bad)
commit (`6cf3ab1`) so you can reproduce and fix the incompatibility
locally by checking out this branch.
_Opened automatically by
[downstream-reports/track-incompatibility](https://github.com/leanprover-community/downstream-reports)
via [this workflow
run](https://github.com/leanprover/cslib/actions/runs/25351406099)._
---------
Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com>
Co-authored-by: Chris Henson <chrishenson.net@gmail.com>1 parent aa62343 commit 02052d4
3 files changed
Lines changed: 4 additions & 4 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
177 | 177 | | |
178 | 178 | | |
179 | 179 | | |
180 | | - | |
| 180 | + | |
181 | 181 | | |
182 | 182 | | |
183 | 183 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
5 | 5 | | |
6 | 6 | | |
7 | 7 | | |
8 | | - | |
| 8 | + | |
9 | 9 | | |
10 | 10 | | |
11 | | - | |
| 11 | + | |
12 | 12 | | |
13 | 13 | | |
14 | 14 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
18 | 18 | | |
19 | 19 | | |
20 | 20 | | |
21 | | - | |
| 21 | + | |
22 | 22 | | |
23 | 23 | | |
24 | 24 | | |
| |||
0 commit comments