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

--- Day changed Sun Jan 08 2017
apostolishttp://lpaste.net/35100508/01 05:13
apostolisI have something like the above but I get an error:08/01 05:13
apostolisFailed to solve the following constraints:[177] _i_38 = _i_182 x : Sizewhen checking that the pattern I has type LFun08/01 05:14
apostolisHere LFun is glog.08/01 05:15
apostolisCan someone exlain to me the error message?08/01 05:16
apostolisI do not see a varriable _i_38 or _i_182.08/01 05:18
apostolisCannot solve variable i of type Size with solution _i_38 because the variable occurs in the solution, or in the type one of the variables in the solution when checking that the pattern I has type LFun08/01 05:23
apostolisAnother error message if I name some of the implicit values.08/01 05:24
Guest32290Is there a "agda without rewrite" primer/tutorial?08/01 20:48
vininimI can see why people like rewrite. This proof seems random (the last x and y swap) http://lpaste.net/35103308/01 22:11

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