From 96f3f480b17bffc258e35eb8739c3ed36c8f6d45 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 20 Dec 2023 12:03:26 +0000
Subject: [PATCH] bump lean toolchain

---
 examples/matching.lean | 2 +-
 lean-toolchain         | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/examples/matching.lean b/examples/matching.lean
index a97fc97..c38bff1 100644
--- a/examples/matching.lean
+++ b/examples/matching.lean
@@ -58,4 +58,4 @@ def pairLit (u : Lean.Level) (α : Q(Type u)) (a : Q($α)) : MetaM Q($α × $α)
   | 0, ~q(Int), z => return q(($z, $z))
   | _, _, _ => failure
 
-#eval do guard <| (←pairLit 0 q(Nat) q(2)) == q((2, 2))
+#eval show MetaM Unit from do guard <| (←pairLit _ _ q(2)) == q((2, 2))
diff --git a/lean-toolchain b/lean-toolchain
index f0a6d66..f90f8ec 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.0.0
+leanprover/lean4-pr-releases:pr-release-3060