mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-01 01:09:03 +03:00
1cf9de4021
`countFrom` must have been made public accidentally: * it is defined in the ranges section of the file, not stream section * it is used only in `Range` implementation * the same function `iterate` is defined in `Data.Stream` ``` countFrom start next ``` is the same as ``` iterate next start ``` |
||
---|---|---|
.. | ||
Prelude | ||
Builtin.idr | ||
Makefile | ||
Prelude.idr | ||
prelude.ipkg | ||
PrimIO.idr |