Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-03 19:44 0ba3098a

View on Github →

chore(data/seq/seq): use terminates predicate in to_list_or_stream (#15826) We already have a canonical way to spell out that a sequence terminates, so we don't need to spell it in full.

Estimated changes