mathlib
0ba3098a
- chore(data/seq/seq): use `terminates` predicate in `to_list_or_stream` (#15826)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
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.
Author
vihdzp
Parents
131c39a4
Loading