Skip to content

Commit f931670

Browse files
committed
chore: naming
1 parent e3882d5 commit f931670

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/Init/Data/BitVec/Lemmas.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6506,14 +6506,14 @@ theorem cpop_reverse (x : BitVec w) :
65066506
simp
65076507

65086508
@[simp]
6509-
theorem cpopNatRec_cast_eq_cpopNatRec_of {x : BitVec w} (p : w = v) :
6509+
theorem cpopNatRec_cast_eq_of_eq {x : BitVec w} (p : w = v) :
65106510
(x.cast p).cpopNatRec n = x.cpopNatRec n := by
65116511
subst p; simp
65126512

65136513
@[simp]
65146514
theorem cpop_cast (h : w = v) (x : BitVec w) :
65156515
(x.cast h).cpop = x.cpop.cast h := by
6516-
simp [cpop, cpopNatRec_cast_eq_cpopNatRec_of, h]
6516+
simp [cpop, cpopNatRec_cast_eq_of_eq, h]
65176517

65186518
@[simp]
65196519
theorem toNat_cpop_append {x : BitVec w} {y : BitVec u} :

0 commit comments

Comments
 (0)