diff --git a/Qq/ForLean/ReduceEval.lean b/Qq/ForLean/ReduceEval.lean
index 97f8577..477fbb3 100644
--- a/Qq/ForLean/ReduceEval.lean
+++ b/Qq/ForLean/ReduceEval.lean
@@ -25,11 +25,18 @@ instance [NeZero n] : ReduceEval (Fin n) where
     else
       throwFailedToEval e
 
+instance {n : Nat} : ReduceEval (BitVec n) where
+  reduceEval := fun e => do
+    let e ← whnf e
+    if e.isAppOfArity ``BitVec.ofFin 2 then
+      pure ⟨(← reduceEval (e.getArg! 1))⟩
+    else
+      throwFailedToEval e
+
 instance : ReduceEval UInt64 where
   reduceEval := fun e => do
     let e ← whnf e
     if e.isAppOfArity ``UInt64.mk 1 then
-      let _ : ReduceEval (Fin UInt64.size) := inferInstanceAs <| ReduceEval (Fin (_ + 1))
       pure ⟨(← reduceEval (e.getArg! 0))⟩
     else
       throwFailedToEval e
diff --git a/lean-toolchain b/lean-toolchain
index eff86fd..22d46f9 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.13.0-rc3
+leanprover/lean4:nightly-2024-10-17