From eed93f832df5bde70c5850404e6a21ef7ab474f8 Mon Sep 17 00:00:00 2001
From: eyihluyc <theviolthevioletandthewine@gmail.com>
Date: Fri, 21 Jun 2024 23:07:33 -0400
Subject: [PATCH] Update toolchain

---
 Minimal/Calculus.lean | 2 +-
 lean-toolchain        | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Minimal/Calculus.lean b/Minimal/Calculus.lean
index 1a76f197..7e39143c 100644
--- a/Minimal/Calculus.lean
+++ b/Minimal/Calculus.lean
@@ -1755,7 +1755,7 @@ def half_diamond
           : Premise l' (complete_developmentLst l)
           := match lst with
             | [] => match l, l' with
-              | Bindings.nil, Bindings.nil => Premise.nil
+              | Bindings.nil, Bindings.nil => by simp; exact Premise.nil
             | a :: as => match premise with
               | Premise.consVoid _ premise_tail => by
                   simp [complete_development]
diff --git a/lean-toolchain b/lean-toolchain
index d8a6d7ef..29c0cea4 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.8.0-rc1
+leanprover/lean4:v4.9.0-rc2