Commit 2026-01-09 08:53 eed70c42

View on Github →

chore(Order/Defs/Unbundled): deprecate IsRefl in favor of core's Std.Refl (#33755)

Estimated changes

modified theorem List.forall₂_refl
modified theorem List.Pairwise.head!_le
modified theorem List.Pairwise.rel_getLast
modified theorem List.Pairwise.rel_get_of_le
modified theorem List.Pairwise.rel_head
modified theorem List.erase_orderedInsert
modified theorem Prod.Lex.refl_left
modified theorem Prod.Lex.refl_right
modified theorem Set.pairwise_iff_of_refl
modified theorem Sum.LiftRel.refl
deleted theorem IsRefl.reflexive
added theorem Std.Refl.reflexive
modified theorem reflexive_ne_imp_iff
modified theorem AntisymmRel.of_eq
modified theorem AntisymmRel.refl
modified theorem AntisymmRel.rfl
modified theorem antisymmRel_iff_eq
modified theorem CompRel.refl
modified theorem CompRel.rfl
modified theorem antisymm_iff
modified theorem of_eq
modified theorem refl
modified theorem refl_of
modified theorem rel_of_subsingleton
modified theorem Filter.isBoundedUnder_const
modified def LatticeCon.mk'
deleted theorem IsRefl.swap
added theorem Std.Refl.swap
modified theorem ne_of_not_subset
modified theorem ne_of_not_superset
modified theorem subset_antisymm_iff
modified theorem subset_iff_ssubset_or_eq
modified theorem subset_of_eq
modified theorem subset_refl
modified theorem subset_rfl
modified theorem superset_antisymm_iff
modified theorem superset_of_eq
modified def RelIso.ofUniqueOfRefl
modified theorem Finite.wellQuasiOrdered
modified theorem Order.le_cof
modified theorem RelIso.cof_eq
modified theorem RelIso.cof_eq_lift