edwinb/Idris-dev — pull request #372 by Melvar (2013-07-03 19:10:51+00:00)
Title: Give replicate a simple total definition

I don’t see a good reason to define `replicate` in terms of `repeat` and `take`, especially given that `repeat` is partial, hence I replaced that definition with the obvious instead.

Indeed I’m not sure `repeat` should exist as is. It would generally be nicer to use streams that guarantee they are infinitely long for such things, but at the least colists.