Commit 2022-05-10 08:56 c8926223
View on Github →move(order/synonym): Group order_dual and lex (#13769)
Move to_dual, of_dual, to_lex, of_lex to a new file order.synonym. This does not change the import tree, because order.lexicographic had slightly higher imports than order.order_dual, but those weren't used for lex itself.