Commit 2021-12-03 08:57 56c9cab5
View on Github →feat(data/sigma{lex,order}): Lexicographic and disjoint orders on a sigma type (#10552) This defines the two natural order on a sigma type: the one where we just juxtapose the summands with their respective order, and the one where we also add in an order between summands.