[Agda] Termination checking on coinduction

[Alex Rozenshteyn]

Wouldn't it also be useful to have a function which returns a Costring
and a proof that it's finite?

That way you'd have a lazy string like in haskell, but you'd be able
to use it in more ways, right?

On Sat, Feb 18, 2012 at 6:30 AM, Nils Anders Danielsson <nad at chalmers.se> wrote:
> 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



-- 
          Alex R