[Agda] Colist -> List

Nils Anders Danielsson nad at chalmers.se
Wed Oct 3 23:13:59 CEST 2012

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


More information about the Agda mailing list