From 1e637dabaa1401d7a9b6fc5743777ea4bbe95fe3 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 13 Sep 2023 21:02:26 -0700
Subject: [PATCH] Bump lean version to 4.0.0

---
 lake-manifest.json | 30 ++++--------------------------
 lean-toolchain     |  2 +-
 2 files changed, 5 insertions(+), 27 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 6a4ca4f..5a13649 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,33 +1,11 @@
-{"version": 4,
+{"version": 5,
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
    {"url": "https://github.com/lurk-lab/LSpec.git",
     "subDir?": null,
     "rev": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
+    "opts": {},
     "name": "LSpec",
-    "inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41"}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/mathlib4.git",
-    "subDir?": null,
-    "rev": "8e5a00a8afc8913c0584cb85f37951995275fd87",
-    "name": "mathlib",
-    "inputRev?": "8e5a00a8afc8913c0584cb85f37951995275fd87"}},
-  {"git":
-   {"url": "https://github.com/gebner/quote4",
-    "subDir?": null,
-    "rev": "c71f94e34c1cda52eef5c93dc9da409ab2727420",
-    "name": "Qq",
-    "inputRev?": "master"}},
-  {"git":
-   {"url": "https://github.com/JLimperg/aesop",
-    "subDir?": null,
-    "rev": "cdc00b640d0179910ebaa9c931e3b733a04b881c",
-    "name": "aesop",
-    "inputRev?": "master"}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "6006307d2ceb8743fea7e00ba0036af8654d0347",
-    "name": "std",
-    "inputRev?": "main"}}]}
+    "inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
+    "inherited": false}}]}
diff --git a/lean-toolchain b/lean-toolchain
index 1acfb77..49fd71c 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-08-12
+leanprover/lean4:4.0.0