Def linear_order.lift
Modification history
2022-07-11 16:51
src/order/basic.lean
fix(order/basic): fix `subtype.linear_order` (#15056) …
Modified linear_order.liftView on Github →2021-06-09 15:40
src/order/basic.lean
fix(*): make some non-instances reducible (#7835) …
Modified linear_order.liftView on Github →2020-06-14 04:30
src/order/basic.lean
refactor(order/basic): make `*order.lift` use `[]` argument (#3067) …
Modified linear_order.liftView on Github →