search

edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
902 stars 58 forks source link

Export 'takeBefore' function #309

Closed ska80 closed 4 years ago

edwinb commented 4 years ago

I'd rather not export this one from the Prelude since it's only there for helping with the range syntax, and is partial, so dosen't really fit with the guidelines for what's in the Prelude. And now I look, I don't think takeUntil should be exported either! I think it would be okay for both in Data.Stream though.

edwinb commented 4 years ago

In fact I've just made that change (exporting the functions from Data.Stream), so I'll close this PR.

ska80 commented 4 years ago

In fact I've just made that change (exporting the functions from Data.Stream), so I'll close this PR.

Thanks! Makes sense.