[Agda] defining coinductive types

[Aaron Stump]

Awesome, thanks. I know it's boring, but I like

fib5h :: Integer -> Integer -> Stream Integer
fib5h n m (OHead f) = f n
fib5h n m (OTail o) = fib5h m (n+m) o

fib5 = fib5h 0 1

pretty well, and this is fast, with and without optimization.

Aaron


On Tue, Dec 17, 2013 at 10:36 AM, Nils Anders Danielsson <nad at cse.gu.se>wrote:

> On 2013-12-17 17:22, Aaron Stump wrote:
>
>> Since I'm not the biggest Haskeller in the world, would you mind
>> making the complete source file you used for testing (I assume you
>> compiled this with ghc, and have a 'main' entrypoint) available to me?
>>
>
> I have attached some code. You can compile it with or without
> optimisations:
>
> * ghc --make Test.hs -O -fforce-recomp
> * ghc --make Test.hs -fforce-recomp
>
> Then you can load it up in GHCi and try things like "take' 35 fib1".
>
> --
> /NAD
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131217/4db5b59a/attachment.html