chore: unsimp BitVec.divRec_succ'

2026-04-05 03:34:08 +00:00 · 2024-09-28 14:58:31 +10:00
1 changed files with 0 additions and 1 deletions
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -799,7 +799,6 @@ theorem umod_eq_divRec (hd : 0#w < d) :
  have := lawful_divRec this
  apply DivModState.umod_eq_of_lawful this (wn_divRec ..)

-@[simp]
 theorem divRec_succ' (m : Nat) (args : DivModArgs w) (qr : DivModState w) :
    divRec (m+1) args qr =
    let wn := qr.wn - 1