From bfef3cb5df05b15c29240425ad1686bbf142b776 Mon Sep 17 00:00:00 2001
From: Julian Berman <Julian@GrayVines.com>
Date: Fri, 17 May 2024 10:52:45 +0300
Subject: [PATCH] Update the Lean version for our sample project.

---
 lua/tests/fixtures/example-project/lean-toolchain | 2 +-
 lua/tests/infoview/contents_spec.lua              | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/lua/tests/fixtures/example-project/lean-toolchain b/lua/tests/fixtures/example-project/lean-toolchain
index 3f21e50b..d8a6d7ef 100644
--- a/lua/tests/fixtures/example-project/lean-toolchain
+++ b/lua/tests/fixtures/example-project/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.5.0-rc1
+leanprover/lean4:v4.8.0-rc1
diff --git a/lua/tests/infoview/contents_spec.lua b/lua/tests/infoview/contents_spec.lua
index c1851d46..77f9c18b 100644
--- a/lua/tests/infoview/contents_spec.lua
+++ b/lua/tests/infoview/contents_spec.lua
@@ -217,10 +217,10 @@ describe('infoview content (auto-)update', function()
       assert.infoview_contents.are [[
         ▶ 2 goals
         case zero
-        ⊢ Nat.zero = Nat.zero
+        ⊢ 0 = 0
         case succ
         n✝ : Nat
-        ⊢ Nat.succ n✝ = Nat.succ n✝
+        ⊢ n✝ + 1 = n✝ + 1
       ]]
     end)