Skip to content

Commit

Permalink
chore: adjust binder
Browse files Browse the repository at this point in the history
  • Loading branch information
hargoniX committed Oct 26, 2024
1 parent 4a1c236 commit 14c4e2a
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Init/Data/BitVec/Lemmas.lean
Original file line number Diff line number Diff line change
Expand Up @@ -2115,7 +2115,7 @@ theorem not_neg (x : BitVec w) : ~~~(-x) = x + -1#w := by

/-! ### abs -/

theorem abs_eq {x : BitVec w} : x.abs = if x.msb then -x else x := by rfl
theorem abs_eq (x : BitVec w) : x.abs = if x.msb then -x else x := by rfl

@[simp, bv_toNat]
theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat else x.toNat := by
Expand Down

0 comments on commit 14c4e2a

Please sign in to comment.