Skip to content

Commit 0344247

Browse files
committed
chore: naming
1 parent 12df67d commit 0344247

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Init/Data/BitVec/Lemmas.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6512,7 +6512,7 @@ theorem cpopNatRec_cast_eq_of_eq {x : BitVec w} (p : w = v) :
65126512
subst p; simp
65136513

65146514
@[simp]
6515-
theorem cpop_cast (h : w = v) (x : BitVec w) :
6515+
theorem cpop_cast (x : BitVec w) (h : w = v) :
65166516
(x.cast h).cpop = x.cpop.cast h := by
65176517
simp [cpop, cpopNatRec_cast_eq_of_eq, h]
65186518

0 commit comments

Comments
 (0)