mathlib3
55a2c1a4 - refactor(set_theory/{cardinal,ordinal}): swap the order of universes in `lift` (#9273)

Commit
4 years ago
refactor(set_theory/{cardinal,ordinal}): swap the order of universes in `lift` (#9273) Swap the order of universe arguments in `cardinal.lift` and `ordinal.lift`. This way (a) they match the order of arguments in `ulift`; (b) usually Lean can deduce the second universe level from the argument.
Author
Parents
Loading