mathlib
3ac9ae73
- chore(data/stream): dedup `take` and `approx` (#10525)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
chore(data/stream): dedup `take` and `approx` (#10525) `stream.take` and `stream.approx` were propositionally equal. Merge them into one function `stream.take`; the definition comes from the old `stream.approx`.
Author
urkud
Parents
bc4ed5c0
Loading