Skip to content

Commit

Permalink
deprecate functions
Browse files Browse the repository at this point in the history
  • Loading branch information
tobiasgrosser committed Oct 27, 2024
1 parent 743a58b commit 062c21b
Showing 1 changed file with 6 additions and 1 deletion.
7 changes: 6 additions & 1 deletion src/Init/Data/BitVec/Lemmas.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1061,7 +1061,6 @@ theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
@[simp] theorem toFin_shiftLeft {n : Nat} (x : BitVec w) :
BitVec.toFin (x <<< n) = Fin.ofNat' (2^w) (x.toNat <<< n) := rfl

-- deprecate?
@[simp]
theorem shiftLeft_zero (x : BitVec w) : x <<< 0 = x := by
apply eq_of_toNat_eq
Expand Down Expand Up @@ -3193,4 +3192,10 @@ abbrev and_one_eq_zeroExtend_ofBool_getLsbD := @and_one_eq_setWidth_ofBool_getLs
@[deprecated msb_sshiftRight (since := "2024-10-03")]
abbrev sshiftRight_msb_eq_msb := @msb_sshiftRight

@[deprecated shiftLeft_zero (since := "2024-10-27")]
abbrev shiftLeft_zero_eq := @shiftLeft_zero

@[deprecated ushiftRight_zero (since := "2024-10-27")]
abbrev ushiftRight_zero_eq := @ushiftRight_zero

end BitVec

0 comments on commit 062c21b

Please sign in to comment.