Bump mathlib

YaelDillies · Jun 14, 2024 · 14694e8 · 14694e8
1 parent 441a6c7
commit 14694e8
Show file tree

Hide file tree

Showing 8 changed files with 8 additions and 92 deletions.
diff --git a/LeanCamCombi.lean b/LeanCamCombi.lean
@@ -44,16 +44,12 @@ import LeanCamCombi.Mathlib.Data.List.Basic
 import LeanCamCombi.Mathlib.Data.List.DropRight
 import LeanCamCombi.Mathlib.Data.Multiset.Basic
 import LeanCamCombi.Mathlib.Data.Nat.Defs
-import LeanCamCombi.Mathlib.Data.Nat.Factors
 import LeanCamCombi.Mathlib.Data.Set.Finite
-import LeanCamCombi.Mathlib.Data.Set.Image
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
 import LeanCamCombi.Mathlib.FieldTheory.Finite.Basic
 import LeanCamCombi.Mathlib.GroupTheory.QuotientGroup
-import LeanCamCombi.Mathlib.Order.Category.BoolAlg
 import LeanCamCombi.Mathlib.Order.ConditionallyCompleteLattice.Basic
 import LeanCamCombi.Mathlib.Order.Hom.Lattice
-import LeanCamCombi.Mathlib.Order.Hom.Set
 import LeanCamCombi.Mathlib.Order.Interval.Finset.Basic
 import LeanCamCombi.Mathlib.Order.Partition.Finpartition
 import LeanCamCombi.Mathlib.Order.Sublattice

diff --git a/LeanCamCombi/Mathlib/Data/Nat/Factors.lean b/LeanCamCombi/Mathlib/Data/Nat/Factors.lean
diff --git a/LeanCamCombi/Mathlib/Data/Set/Image.lean b/LeanCamCombi/Mathlib/Data/Set/Image.lean
diff --git a/LeanCamCombi/Mathlib/Order/Category/BoolAlg.lean b/LeanCamCombi/Mathlib/Order/Category/BoolAlg.lean
diff --git a/LeanCamCombi/Mathlib/Order/Hom/Set.lean b/LeanCamCombi/Mathlib/Order/Hom/Set.lean
diff --git a/LeanCamCombi/Mathlib/Order/SupClosed.lean b/LeanCamCombi/Mathlib/Order/SupClosed.lean
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "6a63eb6a326181df29d95a84ce1f16c1145e66d8",
+   "rev": "15d42e1a92a80d0db5ca1c12123866ba392b9d76",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "7e3bd939c6badfcb1e607c0fddb509548baafd05",
+   "rev": "882561b77bd2aaa98bd8665a56821062bdb3034c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -58,17 +58,17 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "ed63385753ed24f23d780e567364a1e001f6ee91",
+   "rev": "dff3a0ef1acdb1f34dd05dbaa41e620d22c6a3cf",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/xubaiw/CMark.lean",
+  {"url": "https://github.com/acmepjz/md4lean",
    "type": "git",
    "subDir": null,
-   "rev": "ba7b47bd773954b912ecbf5b1c9993c71a166f05",
-   "name": "CMark",
+   "rev": "d812b96744f9b60879cbfa9c436de2b95003db2a",
+   "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
@@ -94,7 +94,7 @@
   {"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
-   "rev": "4e570fed8c4147bdafbd5eada08503ed307252e0",
+   "rev": "b61771aaa8f15bce5e3a38aebeb6dda487f4f29c",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.9.0-rc1
+leanprover/lean4:v4.9.0-rc2
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.9.0-rc1
		leanprover/lean4:v4.9.0-rc2