[Agda] defining coinductive types
aaron-stump at uiowa.edu
Tue Dec 17 20:53:32 CET 2013
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.
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
> * 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".
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda