bump lean toolchain

leanprover-community · Dec 20, 2023 · 96f3f48 · 96f3f48
1 parent c2ab5c3
commit 96f3f48
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -1 +1 @@
-leanprover/lean4:v4.0.0
+leanprover/lean4-pr-releases:pr-release-3060
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.0.0
		leanprover/lean4-pr-releases:pr-release-3060