Skip to content

Commit d1dbe1e

Browse files
authored
chore: Update mathlib revision, fixing a conflict (#467)
[This commit](leanprover-community/mathlib4@ed4fde1#diff-54ef6c59abdddf67950b1ee785a0c22c7e03d04f9ad8cdb7cf1d336a72f4d850) in mathlib4 moves `foldl_eq_foldr` to another module, so we need to import it or the build fails with ```lean error: Cslib/Computability/URM/Basic.lean:178:27: Unknown constant `List.foldl_eq_foldr` ``` This PR updates the lake manifest past this commit with `lake update mathlib` and fixes the issue
1 parent 3875bc9 commit d1dbe1e

2 files changed

Lines changed: 4 additions & 3 deletions

File tree

Cslib/Computability/URM/Basic.lean

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

88
public import Cslib.Computability.URM.Defs
99
public import Mathlib.Data.List.MinMax
10+
public import Mathlib.Data.List.Fold
1011

1112
/-! # URM Basic Lemmas
1213

lake-manifest.json

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "leanprover-community",
8-
"rev": "1a37cd3c8e618022c5e78dee604c75c3c946a681",
8+
"rev": "6ef8cc2731780be866bf243afcb7732f4da5f406",
99
"name": "mathlib",
1010
"manifestFile": "lake-manifest.json",
1111
"inputRev": "master",
@@ -15,7 +15,7 @@
1515
"type": "git",
1616
"subDir": null,
1717
"scope": "leanprover-community",
18-
"rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3",
18+
"rev": "d11647e94d22ea0d9c503af4a63d814f89ea0323",
1919
"name": "plausible",
2020
"manifestFile": "lake-manifest.json",
2121
"inputRev": "main",
@@ -75,7 +75,7 @@
7575
"type": "git",
7676
"subDir": null,
7777
"scope": "leanprover-community",
78-
"rev": "756e3321fd3b02a85ffda19fef789916223e578c",
78+
"rev": "be1a02994ae681d2676c068ebac67a08bf708f96",
7979
"name": "batteries",
8080
"manifestFile": "lake-manifest.json",
8181
"inputRev": "main",

0 commit comments

Comments
 (0)