Mathlib Changelog
v3
Changelog
About
Github
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