From 71f54425e6fe0fa75f3aef33a2813a7898392222 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 9 Aug 2024 01:41:55 +0100
Subject: [PATCH] Bump to Lean v4.10.0 (#49)

One of the new core linters crashes on this test, so for now we disable it.
Since we're touching the test anyway, let's improve the output checking.
---
 examples/hoMatching.lean | 7 ++++++-
 lean-toolchain           | 2 +-
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/examples/hoMatching.lean b/examples/hoMatching.lean
index db8faf2..871b39c 100644
--- a/examples/hoMatching.lean
+++ b/examples/hoMatching.lean
@@ -1,8 +1,13 @@
 import Qq
 open Qq Lean
 
+-- TODO: this linter crashes on the `def` below
+set_option linter.constructorNameAsVariable false in
 def turnExistsIntoForall : Q(Prop) → MetaM Q(Prop)
   | ~q(∃ x y, $p x y) => return q(∀ x y, $p x y)
   | e => return e
 
-#eval turnExistsIntoForall q(∃ a b, String.length a ≤ b + 42)
+/-- info: ∀ (x : String) (y : Nat), x.length ≤ y + 42 -/
+#guard_msgs in
+run_cmd Elab.Command.liftTermElabM do
+  Lean.logInfo <| ← turnExistsIntoForall q(∃ a b, String.length a ≤ b + 42)
diff --git a/lean-toolchain b/lean-toolchain
index 0ba3faf..7f0ea50 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.9.0-rc1
+leanprover/lean4:v4.10.0