chore: adaptations for nightly-2024-10-17 (#60)

* fixes * chore: account for UInt refactoring * simplify --------- Co-authored-by: Henrik Böving <[email protected]> Co-authored-by: Eric Wieser <[email protected]>
leanprover-community · Oct 18, 2024 · 0dc6370 · 0dc6370
1 parent 1357f4f
commit 0dc6370
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 2 deletions.
diff --git 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
@@ -1 +1 @@
-leanprover/lean4:v4.13.0-rc3
+leanprover/lean4:nightly-2024-10-17
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.13.0-rc3
		leanprover/lean4:nightly-2024-10-17