update mathlib

dwrensha · Nov 21, 2023 · 586e6aa · 586e6aa
1 parent e0d3932
commit 586e6aa
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 12 deletions.
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "d3049643f6dded69eb7ce8124796cb1ec8df8840",
+   "rev": "e403f680f0beb8610c29e6f799132e8be880554e",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -28,31 +28,31 @@
    "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
-   "name": "Cli",
+   "rev": "909febc72b4f64628f8d35cd0554f8a90b6e0749",
+   "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v0.0.23",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+  {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "c3b9f0d4ebedc43635d3f7e764e277b1010844b7",
-   "name": "proofwidgets",
+   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.22",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "b5586ed7797c0efb81427ebf7d2412e65959dbf6",
+   "rev": "366aa49a421213f1ab22157d84299da19895f452",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "b5586ed7797c0efb81427ebf7d2412e65959dbf6",
+   "inputRev": "366aa49a421213f1ab22157d84299da19895f452",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "compfiles",

diff --git a/lakefile.lean b/lakefile.lean
@@ -25,4 +25,4 @@ lean_exe checkSolution where
   root := `scripts.checkSolution
   supportInterpreter := true
 
-require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "b5586ed7797c0efb81427ebf7d2412e65959dbf6"
+require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "366aa49a421213f1ab22157d84299da19895f452"