Commit 2021-08-11 18:47 bb29f493

View on Github →

update lean to nightly-2021-08-11 (#32)

Estimated changes

added theorem Array.toArrayLit_eq'
deleted theorem Array.toArrayLit_eq
deleted theorem Nat.eq_zero_or_pos
deleted def Nat.le_add_left
deleted def Nat.le_add_right
deleted def Nat.le_of_lt_succ
deleted def Nat.le_of_succ_le
deleted def Nat.le_step
deleted def Nat.le_succ
deleted def Nat.le_succ_of_le
deleted def Nat.lt_of_succ_le
deleted def Nat.lt_of_succ_lt
deleted def Nat.lt_succ_self
deleted def Nat.not_lt_zero
deleted theorem Nat.not_succ_le_zero
deleted def Nat.pos_pos_of_pos
deleted def Nat.pow_succ
deleted def Nat.pow_zero
deleted def Nat.pred_le
deleted def Nat.pred_le_pred
deleted def Nat.pred_lt
deleted def Nat.sub_le
deleted def Nat.sub_lt
deleted def Nat.succ_eq_add_one
deleted def Nat.succ_le_of_lt
deleted def Nat.succ_le_succ
deleted def Nat.succ_ne_zero
deleted def Nat.succ_pos
deleted def Nat.zero_eq
deleted def Nat.zero_le
deleted def Nat.zero_lt_succ
modified theorem Decidable.not_and
deleted theorem and_false
deleted theorem and_self
deleted theorem and_true
deleted def cast_eq
deleted def cast_heq
deleted theorem dif_eq_if
deleted def dif_neg
deleted def dif_pos
deleted def eq_of_heq
modified def eq_rec_heq
deleted theorem false_and
deleted theorem false_iff
deleted def false_of_ne
deleted theorem false_or
added theorem forall_congr'
deleted theorem forall_congr
deleted def heq_of_eq
deleted def heq_of_eq_of_heq
deleted def heq_of_heq_of_eq
deleted def if_neg
deleted def if_pos
deleted theorem iff_false
deleted theorem iff_self
deleted theorem iff_true
deleted def ne_false_of_self
deleted def ne_true_of_not
deleted def not_false
deleted def of_eq_true
deleted theorem optParam_eq
deleted theorem or_false
deleted theorem or_self
deleted theorem or_true
deleted theorem true_and
deleted theorem true_iff
deleted def true_ne_false
deleted theorem true_or
deleted def type_eq_of_heq
modified theorem Function.surj_inv_eq