Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-07-26 14:25 b8ea20f7

View on Github →

fix(data): bitvec and vector are in the main repo

Estimated changes

Deleted data/bitvec.lean

deleted def bitvec.adc

deleted def bitvec.add_lsb

deleted def bitvec.and

deleted def bitvec.append

deleted def bitvec.bits_to_nat

deleted theorem bitvec.bits_to_nat_to_bool

deleted theorem bitvec.bits_to_nat_to_list

deleted def bitvec.fill_shr

deleted def bitvec.not

deleted theorem bitvec.of_nat_succ

deleted def bitvec.or

deleted def bitvec.sbb

deleted def bitvec.sborrow

deleted def bitvec.sge

deleted def bitvec.sgt

deleted def bitvec.shl

deleted def bitvec.sle

deleted def bitvec.slt

deleted def bitvec.sshr

deleted theorem bitvec.to_nat_append

deleted theorem bitvec.to_nat_of_nat

deleted def bitvec.uborrow

deleted def bitvec.uge

deleted def bitvec.ugt

deleted def bitvec.ule

deleted def bitvec.ult

deleted def bitvec.ushr

deleted def bitvec.xor

deleted def bitvec

Modified data/list/basic.lean

deleted theorem list.eq_nil_of_length_eq_zero

deleted theorem list.length_map₂

deleted theorem list.length_remove_nth

deleted theorem list.length_take

deleted theorem list.length_take_le

deleted def list.map₂

deleted theorem list.ne_nil_of_length_eq_succ

deleted def list.nth_le

deleted def list.remove_nth

deleted def list.update_nth

Modified data/list/comb.lean

deleted theorem list.length_map_accumr

deleted theorem list.length_map_accumr₂

deleted def list.map_accumr

deleted def list.map_accumr₂

Modified data/nat/basic.lean

deleted theorem nat.add_div_left

deleted theorem nat.add_div_right

deleted theorem nat.add_mod_left

deleted theorem nat.add_mod_right

deleted theorem nat.add_mul_div_left

deleted theorem nat.add_mul_div_right

deleted theorem nat.add_mul_mod_self_left

deleted theorem nat.add_mul_mod_self_right

deleted theorem nat.add_one_ne_zero

deleted theorem nat.binary_rec_eq

deleted theorem nat.bitwise_bit

deleted theorem nat.bitwise_bit_aux

deleted theorem nat.bitwise_swap

deleted theorem nat.bitwise_zero

deleted theorem nat.bitwise_zero_left

deleted theorem nat.bitwise_zero_right

deleted theorem nat.bodd_bit

deleted theorem nat.cond_to_bool_mod_two

deleted theorem nat.discriminate

deleted theorem nat.div2_bit

deleted theorem nat.div_mul_le_self

deleted theorem nat.dvd_antisymm

deleted theorem nat.dvd_iff_mod_eq_zero

deleted theorem nat.dvd_mod_iff

deleted theorem nat.dvd_of_mod_eq_zero

deleted theorem nat.dvd_of_mul_dvd_mul_left

deleted theorem nat.dvd_of_mul_dvd_mul_right

deleted theorem nat.dvd_sub

deleted theorem nat.eq_one_of_dvd_one

deleted theorem nat.eq_zero_of_add_eq_zero

deleted theorem nat.eq_zero_of_mul_eq_zero

deleted theorem nat.eq_zero_or_eq_succ_pred

deleted theorem nat.exists_eq_succ_of_ne_zero

deleted def nat.iterate

deleted theorem nat.land_bit

deleted theorem nat.ldiff_bit

deleted theorem nat.le_lt_antisymm

deleted theorem nat.le_mul_self

deleted theorem nat.le_of_dvd

deleted theorem nat.le_succ_of_pred_le

deleted theorem nat.lor_bit

deleted theorem nat.lt_le_antisymm

deleted theorem nat.lt_succ_of_lt

deleted theorem nat.lxor_bit

deleted theorem nat.min_succ_succ

deleted theorem nat.mod_eq_zero_of_dvd

deleted theorem nat.mod_le

deleted theorem nat.mod_pow_succ

deleted theorem nat.mul_div_left

deleted theorem nat.mul_div_right

deleted theorem nat.mul_mod_left

deleted theorem nat.mul_mod_mul_left

deleted theorem nat.mul_mod_mul_right

deleted theorem nat.mul_mod_right

deleted theorem nat.mul_pred_left

deleted theorem nat.mul_pred_right

deleted theorem nat.mul_self_le_mul_self

deleted theorem nat.mul_self_le_mul_self_iff

deleted theorem nat.mul_self_lt_mul_self

deleted theorem nat.mul_self_lt_mul_self_iff

deleted theorem nat.mul_sub_div

deleted theorem nat.one_add

deleted def nat.one_pos

deleted theorem nat.one_shiftl

deleted theorem nat.one_succ_zero

deleted theorem nat.pos_of_dvd_of_pos

deleted theorem nat.pos_pow_of_pos

deleted theorem nat.pow_le_pow_of_le_left

deleted theorem nat.pow_le_pow_of_le_right

deleted theorem nat.pow_lt_pow_of_lt_left

deleted theorem nat.pow_lt_pow_of_lt_right

deleted theorem nat.pow_one

deleted theorem nat.pred_inj

deleted theorem nat.shiftl'_add

deleted theorem nat.shiftl'_sub

deleted theorem nat.shiftl'_tt_eq_mul_pow

deleted theorem nat.shiftl_add

deleted theorem nat.shiftl_eq_mul_pow

deleted theorem nat.shiftl_sub

deleted theorem nat.shiftr_add

deleted theorem nat.shiftr_eq_div_pow

deleted theorem nat.sub_add_min_cancel

deleted theorem nat.sub_eq_sub_min

deleted theorem nat.sub_induction

deleted theorem nat.sub_mul_div

deleted theorem nat.sub_mul_mod

deleted theorem nat.sub_one_sub_lt

deleted theorem nat.succ_add_eq_succ_add

deleted theorem nat.succ_inj

deleted theorem nat.succ_mul_succ_eq

deleted theorem nat.succ_sub

deleted theorem nat.succ_sub_sub_succ

deleted theorem nat.test_bit_bitwise

deleted theorem nat.test_bit_land

deleted theorem nat.test_bit_ldiff

deleted theorem nat.test_bit_lor

deleted theorem nat.test_bit_lxor

deleted theorem nat.test_bit_succ

deleted theorem nat.test_bit_zero

deleted theorem nat.two_step_induction

deleted theorem nat.zero_pow

deleted theorem nat.zero_shiftl

deleted theorem nat.zero_shiftr

Modified data/num/basic.lean

Deleted data/vector.lean

deleted def vector.append

deleted def vector.cons

deleted theorem vector.cons_head_tail

deleted def vector.drop

deleted def vector.elim

deleted def vector.head

deleted theorem vector.head_cons

deleted def vector.length

deleted def vector.map

deleted def vector.map_accumr

deleted def vector.map_accumr₂

deleted theorem vector.map_cons

deleted theorem vector.map_nil

deleted def vector.map₂

deleted def vector.nil

deleted def vector.nth

deleted def vector.of_fn

deleted def vector.remove_nth

deleted def vector.repeat

deleted def vector.tail

deleted theorem vector.tail_cons

deleted def vector.take

deleted def vector.to_list

deleted theorem vector.to_list_append

deleted theorem vector.to_list_cons

deleted theorem vector.to_list_drop

deleted theorem vector.to_list_length

deleted theorem vector.to_list_mk

deleted theorem vector.to_list_nil

deleted theorem vector.to_list_take

deleted def vector