[Agda] Termination checking on coinduction

Alex Rozenshteyn rpglover64 at gmail.com
Sat Feb 18 19:40:15 CET 2012

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

More information about the Agda mailing list