[Agda] Termination checking on coinduction

Nils Anders Danielsson nad at chalmers.se
Sat Feb 18 12:30:54 CET 2012

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).


More information about the Agda mailing list