Commit 2021-08-18 12:21 b14f53b8

View on Github →

feat(Util/Time): #time command

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Int/Basic.lean

modified theorem Int.eq_x_or_neg

deleted theorem Int.eq_zero_ofNatAbs_eq_zero

added theorem Int.eq_zero_of_nat_abs_eq_zero

modified def Int.gcd

deleted theorem Int.mul_negSucc_ofNat_negSucc_ofNat

added theorem Int.mul_neg_succ_of_nat_neg_succ_of_nat

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

added def Int.nat_abs

added theorem Int.nat_abs_eq

added theorem Int.nat_abs_mul_self

added theorem Int.nat_abs_neg

added theorem Int.nat_abs_of_nat

added theorem Int.nat_abs_one

added theorem Int.nat_abs_pos_of_ne_zero

added theorem Int.nat_abs_zero

added def Int.nat_mod

deleted theorem Int.negOfNat_add

deleted theorem Int.negOfNat_eq_subNatNat_zero

deleted theorem Int.negOfNat_mul_negSucc_ofNat

deleted theorem Int.negOfNat_mul_ofNat

deleted theorem Int.negSucc_ofNat_add_negSucc_ofNat

deleted theorem Int.negSucc_ofNat_add_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_mul_negOfNat

deleted theorem Int.negSucc_ofNat_mul_subNatNat

deleted theorem Int.negSucc_ofNat_ofNat

deleted theorem Int.neg_neg_ofNat_succ

added theorem Int.neg_neg_of_nat_succ

deleted theorem Int.neg_ofNat_of_succ

deleted theorem Int.neg_ofNat_zero

added def Int.neg_of_nat

added theorem Int.neg_of_nat_add

added theorem Int.neg_of_nat_eq_sub_nat_nat_zero

added theorem Int.neg_of_nat_mul_neg_succ_of_nat

added theorem Int.neg_of_nat_mul_of_nat

added theorem Int.neg_of_nat_of_succ

added theorem Int.neg_of_nat_zero

added theorem Int.neg_succ_of_nat_add_neg_succ_of_nat

added theorem Int.neg_succ_of_nat_add_of_nat

added theorem Int.neg_succ_of_nat_coe'

added theorem Int.neg_succ_of_nat_coe

added theorem Int.neg_succ_of_nat_eq

added theorem Int.neg_succ_of_nat_inj_iff

added theorem Int.neg_succ_of_nat_mul_neg_of_nat

added theorem Int.neg_succ_of_nat_mul_sub_nat_nat

added theorem Int.neg_succ_of_nat_of_nat

added def Int.nonneg

deleted theorem Int.ofNat_add

deleted theorem Int.ofNat_add_negSucc_ofNat

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_negSucc_ofNat

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

added theorem Int.of_nat_add

added theorem Int.of_nat_add_neg_succ_of_nat

added theorem Int.of_nat_add_of_nat

added theorem Int.of_nat_eq_coe

added theorem Int.of_nat_eq_of_nat_iff

added theorem Int.of_nat_mul

added theorem Int.of_nat_mul_neg_of_nat

added theorem Int.of_nat_mul_neg_succ_of_nat

added theorem Int.of_nat_mul_of_nat

added theorem Int.of_nat_mul_sub_nat_nat

added theorem Int.of_nat_one

added theorem Int.of_nat_sub

added theorem Int.of_nat_succ

added theorem Int.of_nat_zero

deleted theorem Int.sign_mul_natAbs

added theorem Int.sign_mul_nat_abs

deleted theorem Int.subNatNat_add

deleted theorem Int.subNatNat_add_add

deleted theorem Int.subNatNat_add_left

deleted theorem Int.subNatNat_add_negSucc_ofNat

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_of_sub_eq_succ

deleted theorem Int.subNatNat_of_sub_eq_zero

deleted theorem Int.subNatNat_sub

added def Int.sub_nat_nat

added theorem Int.sub_nat_nat_add

added theorem Int.sub_nat_nat_add_add

added theorem Int.sub_nat_nat_add_left

added theorem Int.sub_nat_nat_add_neg_succ_of_nat

added theorem Int.sub_nat_nat_add_right

added theorem Int.sub_nat_nat_elim

added theorem Int.sub_nat_nat_of_le

added theorem Int.sub_nat_nat_of_lt

added theorem Int.sub_nat_nat_of_sub_eq_succ

added theorem Int.sub_nat_nat_of_sub_eq_zero

added theorem Int.sub_nat_nat_sub

modified theorem Int.sub_nat_self

deleted theorem Int.toNat_sub

added def Int.to_nat

added theorem Int.to_nat_sub

Modified Mathlib/Data/List/Card.lean

Modified Mathlib/Data/Subtype.lean

added theorem Subtype.coe_prop

added theorem Subtype.val_eq_coe

modified theorem Subtype.val_prop

Modified Mathlib/Init/Logic.lean

deleted theorem And.left_comm

deleted theorem Bool.ff_ne_tt

added theorem and_left_comm

added theorem bool.ff_ne_tt

Modified Mathlib/Logic/Basic.lean

deleted theorem And.congr_left_iff

deleted theorem And.congr_right_iff

deleted theorem And.imp_left

deleted theorem And.imp_right

deleted theorem And.right_comm

deleted theorem And.rotate

deleted theorem Decidable.iff_iff_not_or_and_or_not

deleted theorem Decidable.not_imp_self

deleted theorem Not.decidable_imp_symm

deleted theorem Not.imp_symm

deleted theorem Or.elim3

deleted theorem and_congr_left'

deleted theorem and_congr_left

deleted theorem and_congr_right'

deleted theorem and_iff_left_iff_imp

deleted theorem and_iff_left_of_imp

deleted theorem and_iff_not_or_not

deleted theorem and_iff_right_iff_imp

deleted theorem and_iff_right_of_imp

deleted theorem and_not_self_iff

deleted theorem and_or_distrib_left

deleted theorem and_or_distrib_right

deleted theorem and_self_left

deleted theorem and_self_right

deleted theorem by_contra

deleted def decidable_of_bool

deleted def decidable_of_iff'

modified def decidable_of_iff

deleted theorem iff_and_self

deleted theorem iff_false_left

deleted theorem iff_false_right

deleted theorem iff_iff_and_or_not_and_not

deleted theorem iff_iff_not_or_and_or_not

deleted theorem iff_mpr_iff_true_intro

deleted theorem iff_not_comm

deleted theorem iff_of_false

deleted theorem iff_of_true

deleted theorem iff_self_and

deleted theorem iff_true_left

deleted theorem iff_true_right

deleted theorem imp.swap

deleted theorem imp_iff_not_or

deleted theorem imp_imp_imp

deleted theorem imp_not_comm

deleted theorem imp_not_self

deleted theorem imp_or_distrib'

deleted theorem imp_or_distrib

deleted theorem not_and'

deleted theorem not_and_distrib

deleted theorem not_and_not_right

deleted theorem not_and_of_not_left

deleted theorem not_and_of_not_or_not

deleted theorem not_and_of_not_right

deleted theorem not_and_self_iff

deleted theorem not_iff

deleted theorem not_iff_comm

deleted theorem not_iff_not

deleted theorem not_imp

deleted theorem not_imp_comm

deleted theorem not_imp_not

deleted theorem not_imp_of_and_not

deleted theorem not_imp_self

deleted theorem not_not

deleted theorem not_or_distrib

deleted theorem not_or_of_imp

deleted theorem of_not_imp

deleted theorem of_not_not

added theorem or.elim3

deleted theorem or_and_distrib_left

deleted theorem or_and_distrib_right

deleted theorem or_iff_left_iff_imp

deleted theorem or_iff_not_and_not

deleted theorem or_iff_not_imp_left

deleted theorem or_iff_not_imp_right

deleted theorem or_iff_right_iff_imp

deleted theorem or_self_left

deleted theorem or_self_right

deleted theorem peirce'

deleted theorem peirce

deleted theorem xor_comm

deleted theorem xor_false

deleted theorem xor_self

deleted theorem xor_true

Deleted Mathlib/Tactic/Coe.lean

Created Mathlib/Util/Time.lean

added def timeCmdElab