cleanup

leanprover · Nov 6, 2024 · 66ac702 · 66ac702
1 parent 11743c3
commit 66ac702
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/src/Lean/SimpLC/Whitelists/BitVec.lean b/src/Lean/SimpLC/Whitelists/BitVec.lean
@@ -11,9 +11,6 @@ import Std.Tactic.BVDecide
 simp_lc ignore BitVec.getLsbD_ge
 simp_lc ignore BitVec.getMsbD_ge
 
--- TODO: this one indicates some work required around `Fin.ofNat'`
-simp_lc whitelist BitVec.ofFin_sub BitVec.sub_zero
-
 -- TODO: move to library
 @[simp] theorem Fin.ofNat'_zero (n : Nat) [NeZero n] : Fin.ofNat' n 0 = 0 := rfl