Commit 2017-07-26 14:25 b8ea20f7

View on Github →

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

Estimated changes

deleted def bitvec.adc
deleted def bitvec.add_lsb
deleted def bitvec.and
deleted def bitvec.append
deleted def bitvec.bits_to_nat
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
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 def list.nth_le
deleted def list.remove_nth
deleted def list.update_nth
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_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_sub
deleted theorem nat.eq_one_of_dvd_one
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_lt_mul_self
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_lt_pow_of_lt_left
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
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 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