Commit 2025-03-17 06:31 0954888d

View on Github →

chore: delete more Deprecated files (#22485) As the one who pushed for and ultimately effected their deprecation it is only fitting that I be the one to make the PR that removes them.

Estimated changes

deleted def AsFalse
deleted theorem AsTrue.get
deleted def AsTrue
deleted def Associative
deleted def Commutative
deleted def IsDecEq
deleted def IsDecRefl
deleted def LeftCancelative
deleted def LeftDistributive
deleted def LeftIdentity
deleted def RightCancelative
deleted def RightDistributive
deleted def RightIdentity
deleted def RightInverse
deleted theorem and_false_iff
deleted theorem and_true_iff
deleted theorem cast_proof_irrel
deleted theorem decidableEq_inl_refl
deleted theorem decidableEq_inr_neg
deleted theorem decide_False'
deleted theorem decide_True'
deleted theorem dif_ctx_congr
deleted theorem dif_ctx_simp_congr
deleted theorem eq_rec_compose
deleted theorem false_and_iff
deleted theorem false_iff_iff
deleted theorem false_or_iff
deleted theorem heq_of_eq_rec_left
deleted theorem heq_of_eq_rec_right
deleted theorem if_congr_prop
deleted theorem if_ctx_congr_prop
deleted theorem if_ctx_simp_congr_prop
deleted theorem if_simp_congr_prop
deleted theorem iff_false_iff
deleted theorem iff_self_iff
deleted theorem iff_true_iff
deleted theorem imp_of_if_neg
deleted theorem imp_of_if_pos
deleted theorem let_body_eq
deleted theorem let_eq
deleted theorem let_value_eq
deleted theorem let_value_heq
deleted theorem of_heq_true
deleted theorem or_false_iff
deleted theorem or_true_iff
deleted theorem rec_subsingleton
deleted theorem true_and_iff
deleted theorem true_iff_iff
deleted theorem true_or_iff
deleted theorem max_associative
deleted theorem max_commutative
deleted theorem min_associative
deleted theorem min_commutative