[Agda] Side Effects in Agda

[Andreas Abel]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 24.03.2014 17:16, Joe M wrote:
> Just wanted to check if there are any plans to implement Idris 
> side-effects in Agda.

Not that I heard of.

You are welcome to do it!  I guess this would amount to a library of
effects written in Agda and a foreign-function interface for them.

Cheers,
Andreas

- -- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.11 (GNU/Linux)
Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/

iEYEARECAAYFAlMwYC4ACgkQPMHaDxpUpLOvDQCdFVcLx7hfwS7cv1/EITnZUFZb
ePgAoK0x+JVG8SateO7xHGIccTRDI4rJ
=DtE9
-----END PGP SIGNATURE-----