Skip to content

Commit 4e1b076

Browse files
fgdoraisleanprover-community-mathlib4-botkim-em
committed
chore: adaptations for batteries#1503 (#31422)
After [batteries#1503](leanprover-community/batteries#1503) is merged: - [x] Edit the lakefile to point to leanprover-community/batteries:main - [x] Run lake update batteries - [x] Merge leanprover-community/mathlib4:master - [x] Wait for CI and merge Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: F. G. Dorais <fgdorais@gmail.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
1 parent 5d2ad00 commit 4e1b076

File tree

5 files changed

+2
-159
lines changed

5 files changed

+2
-159
lines changed

Mathlib.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3497,7 +3497,6 @@ import Mathlib.Data.List.ProdSigma
34973497
import Mathlib.Data.List.Range
34983498
import Mathlib.Data.List.ReduceOption
34993499
import Mathlib.Data.List.Rotate
3500-
import Mathlib.Data.List.Scan
35013500
import Mathlib.Data.List.Sections
35023501
import Mathlib.Data.List.Shortlex
35033502
import Mathlib.Data.List.Sigma

Mathlib/Data/List/Scan.lean

Lines changed: 0 additions & 155 deletions
This file was deleted.

Mathlib/Data/Vector/Basic.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,6 @@ Authors: Mario Carneiro
66
import Mathlib.Data.Vector.Defs
77
import Mathlib.Data.List.Nodup
88
import Mathlib.Data.List.OfFn
9-
import Mathlib.Data.List.Scan
109
import Mathlib.Control.Applicative
1110
import Mathlib.Control.Traversable.Basic
1211
import Mathlib.Algebra.BigOperators.Group.List.Basic

lake-manifest.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,7 @@
6565
"type": "git",
6666
"subDir": null,
6767
"scope": "leanprover-community",
68-
"rev": "65d5bc0f949f10d33fb61d9ab87dceb6f62d036e",
68+
"rev": "754186a55901dcfdfd4a15f0e4217d8dce65ac37",
6969
"name": "batteries",
7070
"manifestFile": "lake-manifest.json",
7171
"inputRev": "main",

lakefile.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ open Lake DSL
66
## Mathlib dependencies on upstream projects
77
-/
88

9-
require "leanprover-community" / "batteries" @ git "main"
9+
require "leanprover-community" / "batteries" @ "main"
1010
require "leanprover-community" / "Qq" @ git "master"
1111
require "leanprover-community" / "aesop" @ git "master"
1212
require "leanprover-community" / "proofwidgets" @ git "v0.0.77" -- ProofWidgets should always be pinned to a specific version

0 commit comments

Comments
 (0)