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

--- Day changed Sat Jul 15 2017
jonsterlingi'm not sure where it is documented, but that projection notation has been usable for at least a few months. it's helpful when defining objects by copatterns especially!15/07 03:55
rntzjonsterling: is there a reason it's more useful for defining objects by copatterns than the usual prefix syntax?15/07 14:26
rntzdo you just like the way it looks more, or is there some concrete thing one can do the other can't?15/07 14:26
carterrntz: copatterns rock15/07 14:51
carterThey only really shine for coinductive records but they are magic15/07 14:52
rntz... yes, I know about copatterns15/07 15:57
rntzwhy are *postfix* copatterns specifically useful15/07 15:57
mietekI was unable to find a reference for the new notation15/07 20:40

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