From 7be8472ae3f14cf44c0ffe3f583e117f04a354d2 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@lean-fro.org>
Date: Sat, 10 Aug 2024 13:28:30 +0200
Subject: [PATCH] chore: bump Lean and Verso (#19)

This includes the improvements to inductive type docstring rendering in
Verso.
---
 lake-manifest.json | 2 +-
 lean-toolchain     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 10450df..0008cbd 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d0855a766c98af34f1ffaacd1858a8cca6c5e71c",
+   "rev": "000647872db8486c7f520f3c411134a8a9c9868e",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lean-toolchain b/lean-toolchain
index 9f1d286..542de75 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-07-12
+leanprover/lean4:nightly-2024-08-10
\ No newline at end of file