Commit 2026-04-02 06:37 8a623d70
View on Github →chore: use a type synonym instead of an abbrev for Interval (#37508)
Otherwise, there are conflicting instances between Interval and its definition WithBot ..., creating diamonds: the multiplication is not defined in the same way (on WithBot, we have 0 * bot = 0 while on Interval we have 0 * bot = bot), and the nsmul fields are also different.