simplify

leanprover-community · Oct 18, 2024 · c20ed8d · c20ed8d
1 parent e141ac3
commit c20ed8d
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/Qq/ForLean/ReduceEval.lean b/Qq/ForLean/ReduceEval.lean
@@ -29,8 +29,6 @@ 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