From 1357f4f49450abb9dfd4783e38219f4ce84f9785 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 18 Oct 2024 16:35:39 +0100
Subject: [PATCH 1/2] feat: generalize `ReduceEval (Fin n)` to use `NeZero`
 (#61)

This requires a toolchain bump.
---
 Qq/ForLean/ReduceEval.lean | 4 ++--
 lean-toolchain             | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Qq/ForLean/ReduceEval.lean b/Qq/ForLean/ReduceEval.lean
index a3f664e..97f8577 100644
--- a/Qq/ForLean/ReduceEval.lean
+++ b/Qq/ForLean/ReduceEval.lean
@@ -17,11 +17,11 @@ private partial def evalList [ReduceEval α] (e : Expr) : MetaM (List α) := do
 
 instance [ReduceEval α] : ReduceEval (List α) := ⟨evalList⟩
 
-instance : ReduceEval (Fin (n+1)) where
+instance [NeZero n] : ReduceEval (Fin n) where
   reduceEval := fun e => do
     let e ← whnf e
     if e.isAppOfArity ``Fin.mk 3 then
-      return Fin.ofNat (← reduceEval (e.getArg! 1))
+      return Fin.ofNat' _ (← reduceEval (e.getArg! 1))
     else
       throwFailedToEval e
 
diff --git a/lean-toolchain b/lean-toolchain
index 98556ba..eff86fd 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.12.0-rc1
+leanprover/lean4:v4.13.0-rc3

From d6ae727639429892c372d613b31967b6ee51f78c Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sat, 2 Nov 2024 14:35:55 +0000
Subject: [PATCH 2/2] =?UTF-8?q?style:=20replace=20`=E2=86=90=20pure`=20wit?=
 =?UTF-8?q?h=20`:=3D`=20in=20matches=20(#63)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Qq/ForLean/ReduceEval.lean | 2 +-
 Qq/Macro.lean              | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Qq/ForLean/ReduceEval.lean b/Qq/ForLean/ReduceEval.lean
index 97f8577..fe14353 100644
--- a/Qq/ForLean/ReduceEval.lean
+++ b/Qq/ForLean/ReduceEval.lean
@@ -8,7 +8,7 @@ def throwFailedToEval (e : Expr) : MetaM α :=
 
 private partial def evalList [ReduceEval α] (e : Expr) : MetaM (List α) := do
   let e ← whnf e
-  let .const c _ ← pure e.getAppFn | throwFailedToEval e
+  let .const c _ := e.getAppFn | throwFailedToEval e
   let nargs := e.getAppNumArgs
   match c, nargs with
     | ``List.nil, 1 => pure []
diff --git a/Qq/Macro.lean b/Qq/Macro.lean
index 4c52ba7..4f1a5ea 100644
--- a/Qq/Macro.lean
+++ b/Qq/Macro.lean
@@ -254,7 +254,7 @@ partial def unquoteExpr (e : Expr) : UnquoteM Expr := do
     }
     return fv
   let e ← whnf e
-  let .const c _ ← pure e.getAppFn | throwError "unquoteExpr: {e} : {eTy}"
+  let .const c _ := e.getAppFn | throwError "unquoteExpr: {e} : {eTy}"
   let nargs := e.getAppNumArgs
   match c, nargs with
     | ``betaRev', 2 => return betaRev' (← unquoteExpr (e.getArg! 0)) (← unquoteExprList (e.getArg! 1))