[Agda] defining coinductive types

[Nils Anders Danielsson]

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 --------------
A non-text attachment was scrubbed...
Name: Test.hs
Type: text/x-haskell
Size: 1259 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20131217/6088c36d/Test.bin