Update toolchain

objectionary · Jun 22, 2024 · eed93f8 · eed93f8
1 parent d88e099
commit eed93f8
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -1 +1 @@
-leanprover/lean4:v4.8.0-rc1
+leanprover/lean4:v4.9.0-rc2
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.8.0-rc1
		leanprover/lean4:v4.9.0-rc2