Left-closed right-open order interval

Stream: Is there code for X?

[Will Crichton]

I would like a NonemptyInterval-style interface but for left-closed right-open intervals, such as Set.Ico. Does this exist anywhere?

[Daniel Weber]

@loogle Prod.fst _ < Prod.snd _

[loogle]

:search: Finset.offDiag_filter_lt_eq_filter_le, Finset.sum_sym2_filter_not_isDiag, and 3 more

[Yaël Dillies]

This doesn't exist, no. You could just reuse NonemptyInterval by defining a function NonemptyInterval.toIco which does the obvious thing, but it will send all [a, a] to ∅. I think this is fine and I doubt it's worth making a subtype since it wouldn't even be a lattice.