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

--- Day changed Sat Nov 07 2015
tomjackhmm. isn't `suc (max m n)` there green slime?07/11 02:22
tomjackthe `max` specifically?07/11 02:22
tomjacksee https://personal.cis.strath.ac.uk/conor.mcbride/Pivotal.pdf for the meaning of "green slime"07/11 02:29
tomjackI kind of like "functions in the return type of constructors" better than "green slime"07/11 02:30
tomjackI didn't mean to imply conor's connotation, but it does make me think that functions in type signatures _there_ is not the whole point :)07/11 02:31

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