PR #18750 feat(order/rel_classes): housekeeping

feat(order/rel_classes): housekeeping #18750

vihdzp wants to merge 4 commits into master from wf_cleanup_1

cleanup

3ba74c2e

vihdzp added awaiting-review

these are all automatically inferred

07c4504d

vihdzp added modifies-synchronized-file

vihdzp added t-order

instance

4fdb452f

Merge branch 'hydra_typeclass' into wf_cleanup_1

deccad69

mathlib-dependent-issues-bot added blocked-by-other-PR

eric-wieser added not-too-late

Reviewers

No reviews

Assignees

No one assigned

Labels

awaiting-review blocked-by-other-PR t-order modifies-synchronized-file not-too-late

Milestone

No milestone