Commit 2022-09-08 13:17 d75314b3

View on Github →

fix(data/nat/interval): do not dedup when implementing finset.Icc etc (#16423) This means that finset.Iic n no longer has quadratic complexity. #eval (finset.Iic 200000).card is now almost instant rather than taking a very long time.

Estimated changes

Modified src/data/nat/interval.lean

modified theorem nat.Icc_eq_range'

modified theorem nat.Ico_eq_range'

modified theorem nat.Ioc_eq_range'

modified theorem nat.Ioo_eq_range'

modified theorem nat.card_Icc

modified theorem nat.card_Ico

modified theorem nat.card_Ioc

modified theorem nat.card_Ioo