merge lean-pr-testing-5323

Qq/ForLean/ReduceEval.lean

@@ -25,11 +25,20 @@ instance : ReduceEval (Fin (n+1)) 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
+      have : 2^n - 1 + 1 = 2^n := Nat.sub_one_add_one_eq_of_pos (Nat.two_pow_pos n)
+      let _ : ReduceEval (Fin (2^n)) := this ▸ (inferInstanceAs <| ReduceEval (Fin (2^n - 1 + 1)))
+      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