/home/laney/.irssi/irclogs/Freenode/#agda.log-20170107

--- Day changed Fri Jan 06 2017
IronicDeathso what exactly is type theory?06/01 03:26
* Taneb has written a brainfuck interpeter in Agda06/01 13:37
TanebGonna test it when I can get it to compile06/01 13:37
Tanebhttps://gist.github.com/Taneb/a4e166c913265f837f2216fa5e707b9506/01 14:39
{AS}Taneb: isn't the idea of using Colist that your program is terminating? :)06/01 14:41
Taneb{AS}, well, input (and output) can be productively infinite06/01 14:42
TanebBut the actual execution of the program can be unproductively infinite06/01 14:42
Taneb(for example, the brainfuck program "+[]")06/01 14:42
{AS}I see06/01 14:43

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!