Commit 2022-09-06 13:11 d6824653

View on Github →

chore: update lean + std4 09-05 (#401)

Estimated changes

deleted theorem Int.add_assoc_aux1
deleted theorem Int.add_assoc_aux2
added theorem Int.coe_nat_le
added theorem Int.coe_nat_lt
deleted theorem Int.eq_x_or_neg
deleted def Int.fdiv
deleted def Int.fmod
deleted def Int.gcd
deleted theorem Int.natAbs_eq
deleted theorem Int.natAbs_mul_self
deleted theorem Int.natAbs_neg
deleted theorem Int.natAbs_ofNat
deleted theorem Int.natAbs_one
deleted theorem Int.natAbs_pos_of_ne_zero
deleted theorem Int.natAbs_zero
deleted theorem Int.negOfNat_add
deleted theorem Int.negOfNat_mul_ofNat
deleted theorem Int.negSucc_ofNat_coe'
deleted theorem Int.negSucc_ofNat_coe
deleted theorem Int.negSucc_ofNat_eq
deleted theorem Int.negSucc_ofNat_inj_iff
deleted theorem Int.negSucc_ofNat_ofNat
deleted theorem Int.neg_neg_ofNat_succ
deleted theorem Int.neg_ofNat_of_succ
deleted theorem Int.neg_ofNat_zero
deleted theorem Int.ofNat_add
deleted theorem Int.ofNat_add_ofNat
deleted theorem Int.ofNat_eq_ofNat_iff
deleted theorem Int.ofNat_mul
deleted theorem Int.ofNat_mul_negOfNat
deleted theorem Int.ofNat_mul_ofNat
deleted theorem Int.ofNat_mul_subNatNat
deleted theorem Int.ofNat_one
deleted theorem Int.ofNat_sub
deleted theorem Int.ofNat_succ
deleted theorem Int.ofNat_zero
deleted def Int.quot
deleted def Int.rem
deleted def Int.sign
deleted theorem Int.sign_mul_natAbs
deleted theorem Int.sign_neg_one
deleted theorem Int.sign_one
deleted theorem Int.sign_zero
deleted theorem Int.subNatNat_add
deleted theorem Int.subNatNat_add_add
deleted theorem Int.subNatNat_add_left
deleted theorem Int.subNatNat_add_right
deleted theorem Int.subNatNat_elim
deleted theorem Int.subNatNat_of_le
deleted theorem Int.subNatNat_of_lt
deleted theorem Int.subNatNat_sub
deleted theorem Int.sub_nat_self
deleted theorem Int.toNat_sub
deleted theorem Int.NonNeg.elim
deleted theorem Int.add_one_le_of_lt
deleted theorem Int.eq_natAbs_of_zero_le
deleted theorem Int.eq_ofNat_of_zero_le
deleted theorem Int.eq_succ_of_zero_lt
deleted theorem Int.exists_eq_neg_ofNat
deleted theorem Int.le.dest
deleted theorem Int.le.dest_sub
deleted theorem Int.le.intro
deleted theorem Int.le.intro_sub
deleted theorem Int.le_def
deleted theorem Int.le_natAbs
deleted theorem Int.le_of_lt
deleted theorem Int.le_of_lt_add_one
deleted theorem Int.le_of_sub_one_lt
deleted theorem Int.le_sub_one_of_lt
deleted theorem Int.lt.dest
deleted theorem Int.lt.intro
deleted theorem Int.lt_add_one_of_le
deleted theorem Int.lt_add_succ
deleted theorem Int.lt_iff_add_one_le
deleted theorem Int.lt_of_add_one_le
deleted theorem Int.lt_of_le_sub_one
deleted theorem Int.lt_succ
deleted theorem Int.natAbs_of_nonneg
deleted theorem Int.neg_succ_lt_zero
deleted theorem Int.nonneg_def
deleted theorem Int.nonneg_or_nonneg_neg
deleted theorem Int.ofNat_le
deleted theorem Int.ofNat_lt
deleted theorem Int.ofNat_nonneg
deleted theorem Int.ofNat_succ_pos
deleted theorem Int.ofNat_zero_le
deleted theorem Int.pos_of_sign_eq_one
deleted theorem Int.sign_eq_one_iff_pos
deleted theorem Int.sign_eq_one_of_pos
deleted theorem Int.sign_eq_zero_iff_zero
deleted theorem Int.sign_of_succ
deleted theorem Int.sub_one_lt_of_le
deleted theorem Not.imp
deleted theorem Or.imp
deleted theorem Or.imp_left
deleted theorem Or.imp_right
deleted structure Tactic.NormCast.CoeFnInfo
deleted inductive Tactic.NormCast.CoeFnType
deleted inductive Tactic.NormCast.Label