Commit 2025-12-23 12:58 9f92d5fc

View on Github →

chore(Order/Defs/Unbundled): deprecate EmptyRelation in favor of core's emptyRelation (#33204)

Estimated changes

deleted def EmptyRelation
modified theorem empty_relation_apply
modified theorem eq_empty_relation
modified theorem Ordinal.type_empty
modified theorem Ordinal.type_pEmpty
modified theorem Ordinal.type_pUnit
modified theorem Ordinal.type_unit