Skip to content

Commit 4f59b5c

Browse files
committed
adaptations for leanprover/lean4#11620
1 parent c49c6fc commit 4f59b5c

File tree

4 files changed

+2
-5
lines changed

4 files changed

+2
-5
lines changed

Mathlib/Data/Nat/Find.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@ module
77

88
public import Mathlib.Data.Nat.Basic
99
public import Mathlib.Tactic.Push
10-
public import Batteries.WF
1110

1211
/-!
1312
# `Nat.find` and `Nat.findGreatest`

Mathlib/Data/PFun.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,6 @@ Authors: Mario Carneiro, Jeremy Avigad, Simon Hudon
55
-/
66
module
77

8-
public import Batteries.WF
98
public import Batteries.Tactic.GeneralizeProofs
109
public import Mathlib.Data.Part
1110
public import Mathlib.Data.Rel

Mathlib/Order/RelClasses.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@ module
88
public import Mathlib.Logic.IsEmpty
99
public import Mathlib.Order.Basic
1010
public import Mathlib.Tactic.MkIffOfInductiveProp
11-
public import Batteries.WF
1211

1312
/-!
1413
# Unbundled relation classes

lake-manifest.json

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@
4545
"type": "git",
4646
"subDir": null,
4747
"scope": "leanprover-community",
48-
"rev": "8e37a9bed06d16a2c4253ee62938e216d3fc9a3a",
48+
"rev": "f299cb34cf8d828481e621e1b680734b4ecc59f2",
4949
"name": "aesop",
5050
"manifestFile": "lake-manifest.json",
5151
"inputRev": "nightly-testing",
@@ -65,7 +65,7 @@
6565
"type": "git",
6666
"subDir": null,
6767
"scope": "leanprover-community",
68-
"rev": "382e3416a614bcf0e2441977c173122e5e84b75f",
68+
"rev": "df64ff0042624aa48bb9ede80011b22e738413b2",
6969
"name": "batteries",
7070
"manifestFile": "lake-manifest.json",
7171
"inputRev": "lean-pr-testing-11620",

0 commit comments

Comments
 (0)