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

@@ -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)

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.9.0-rc1
+leanprover/lean4:v4.10.0