[Agda] Termination checking on coinduction

[Nils Anders Danielsson]

On 2012-02-18 00:03, Alex Rozenshteyn wrote:
> I'm trying to write a relatively trivial (or so I thought) program
> that does IO which takes a file containing a newline separated list of
> decimal numbers and outputs the largest one.
>
> I guess if I validate the input (and rule out numbers longer than an
> arbitrary number of digits) and postulate that the file is of bounded
> size, I could do it.
>
> Any advice?

I just added IO.readFiniteFile, which returns a String rather than a
Costring (and raises an exception if you try to read /dev/zero).

-- 
/NAD