[Agda] Colist -> List

[Nils Anders Danielsson]

On 2012-10-03 01:20, Andreas Abel wrote:
> Here is a snippet from Prelude.agda (F. Kettelhoit) that uses the
> dirty trick of cutting a line at some arbitrary maximal length.

The standard library contains a function which reads a /finite/ file and
gives you a string:

   -- Reads a finite file. Raises an exception if the file path refers to
   -- a non-physical file (like "/dev/zero").

   readFiniteFile : String → IO String

-- 
/NAD