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

--- Day changed Wed May 10 2017
rgrinberghow does partial application work in agda with mixfix operators?10/05 21:42
rgrinbergFor example, is it possible to apply the 2nd argument in ::?10/05 21:43
mietek_:: foo10/05 21:43
rgrinbergmietek: thanks10/05 21:49
rgrinbergis there a way to apply a particular implicit argument?10/05 22:07
gallais_rgrinberg: by name (e.g. foo {t = expr})10/05 22:38
gallais_If you have a mixfix function name, you'll have to use it in a prefix manner10/05 22:38
mietekyes. this is unfortunate.10/05 23:08

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