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

--- Day changed Tue Jun 13 2017
mietekyes13/06 00:05
mietekit’s quite free-form13/06 00:05
Nik05thank you mietek, totally looked over your reaction13/06 09:24
Nik05Im reading through Agda.Induction and it is pretty interesting how induction is defined13/06 13:09
Nik05Can I do a case split or destruction in a lambda?13/06 14:57
Nik05If there is just one case?13/06 14:58
comietekNik05: yes, you need more syntactic noise13/06 15:13
comietek\lambda { (x , y) -> x }13/06 15:14
Nik05thank you comietek 13/06 15:15
Nik05I could ofcourse also use where and make a subfunction?13/06 15:16
Nik05Guess I cant do it because the two arguments are depending on eachother, so I need to do a case split on both13/06 15:18

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