chore: account for UInt refactoring

leanprover-community · Sep 23, 2024 · 6e87b74 · 6e87b74
1 parent 2c8ae45
commit 6e87b74
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 2 deletions.
diff --git a/Qq/ForLean/ReduceEval.lean b/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

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.12.0-rc1
+leanprover/lean4-pr-releases:pr-release-5323
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.12.0-rc1
		leanprover/lean4-pr-releases:pr-release-5323