Skip to content

Commit

Permalink
chore: complete deprecations
Browse files Browse the repository at this point in the history
  • Loading branch information
tobiasgrosser committed Sep 18, 2024
1 parent e04acea commit c8a00ed
Showing 1 changed file with 73 additions and 0 deletions.
73 changes: 73 additions & 0 deletions src/Init/Data/BitVec/Lemmas.lean
Original file line number Diff line number Diff line change
Expand Up @@ -2174,6 +2174,79 @@ abbrev msb_truncate := @msb_setWidth
@[deprecated cast_setWidth (since := "2024-09-18")]
abbrev cast_zeroExtend := @cast_setWidth

@[deprecated cast_setWidth (since := "2024-09-18")]
abbrev cast_truncate := @cast_setWidth

@[deprecated setWidth_setWidth_of_le (since := "2024-09-18")]
abbrev zeroExtend_zeroExtend_of_le := @setWidth_setWidth_of_le

@[deprecated setWidth_eq (since := "2024-09-18")]
abbrev truncate_eq_self := @setWidth_eq

@[deprecated setWidth_cast (since := "2024-09-18")]
abbrev truncate_cast := @setWidth_cast

@[deprecated msb_setWidth (since := "2024-09-18")]
abbrev mbs_zeroExtend := @msb_setWidth

@[deprecated msb_setWidth' (since := "2024-09-18")]
abbrev mbs_zeroExtend' := @msb_setWidth'

@[deprecated setWidth_one_eq_ofBool_getLsb_zero (since := "2024-09-18")]
abbrev zeroExtend_one_eq_ofBool_getLsb_zero := @setWidth_one_eq_ofBool_getLsb_zero

@[deprecated setWidth_ofNat_one_eq_ofNat_one_of_lt (since := "2024-09-18")]
abbrev zeroExtend_ofNat_one_eq_ofNat_one_of_lt := @setWidth_ofNat_one_eq_ofNat_one_of_lt

@[deprecated setWidth_one (since := "2024-09-18")]
abbrev truncate_one := @setWidth_one

@[deprecated setWidth_ofNat_of_le (since := "2024-09-18")]
abbrev truncate_ofNat_of_le := @setWidth_ofNat_of_le

@[deprecated setWidth_or (since := "2024-09-18")]
abbrev truncate_or := @setWidth_or

@[deprecated setWidth_and (since := "2024-09-18")]
abbrev truncate_and := @setWidth_and

@[deprecated setWidth_xor (since := "2024-09-18")]
abbrev truncate_xor := @setWidth_xor

@[deprecated setWidth_not (since := "2024-09-18")]
abbrev truncate_not := @setWidth_not

@[deprecated signExtend_eq_not_setWidth_not_of_msb_false (since := "2024-09-18")]
abbrev signExtend_eq_not_zeroExtend_not_of_msb_false := @signExtend_eq_not_setWidth_not_of_msb_false

@[deprecated signExtend_eq_not_setWidth_not_of_msb_true (since := "2024-09-18")]
abbrev signExtend_eq_not_zeroExtend_not_of_msb_true := @signExtend_eq_not_setWidth_not_of_msb_true

@[deprecated signExtend_eq_setWidth_of_lt (since := "2024-09-18")]
abbrev signExtend_eq_truncate_of_lt := @signExtend_eq_setWidth_of_lt

@[deprecated truncate_append (since := "2024-09-18")]
abbrev truncate_append := @setWidth_append

@[deprecated truncate_append_of_eq (since := "2024-09-18")]
abbrev truncate_append_of_eq := @setWidth_append_of_eq

@[deprecated truncate_cons (since := "2024-09-18")]
abbrev truncate_cons := @setWidth_cons

@[deprecated truncate_succ (since := "2024-09-18")]
abbrev truncate_succ := @setWidth_succ

@[deprecated truncate_add (since := "2024-09-18")]
abbrev truncate_add := @setWidth_add

@[deprecated setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false (since := "2024-09-18")]
abbrev zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false := @setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false

@[deprecated setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true (since := "2024-09-18")]
abbrev zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true := @setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true

@[deprecated and_one_eq_setWidth_ofBool_getLsbD (since := "2024-09-18")]
abbrev and_one_eq_zeroExtend_ofBool_getLsbD := @and_one_eq_setWidth_ofBool_getLsbD

end BitVec

0 comments on commit c8a00ed

Please sign in to comment.