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

--- Day changed Fri Apr 14 2017
subttlegah, okay, I see where I was wrong now14/04 00:02
subttlecomietek: that wasn't exactly what I needed but it helped!14/04 00:02
subttleit turns out I had Fin′ and Fin mixed up in a few places :D14/04 00:02
comietekok. Not sure what Fin' is14/04 01:05
subttlehttps://github.com/agda/agda-stdlib/blob/master/src/Data/Fin.agda#L4114/04 02:33
subttleI was just playing around with different ways of implementing a DFA14/04 18:14
subttleI think this one is best, so far14/04 18:14
subttlehttps://gist.github.com/subttle/617a09b0668bb4246d4cf2b11bb497e514/04 18:14
subttleI'm going to try and improve and expand upon that14/04 18:15
subttlethis might be the most fun I've ever had, Agda is amazing I'm learning so much14/04 18:16
akr[m]> δ⋆ = foldl (curry δ)14/04 18:38
lambdabot <hint>:1:4: error:14/04 18:38
lambdabot     parse error on input ‘=’14/04 18:38
lambdabot     Perhaps you need a 'let' in a 'do' block?14/04 18:38
akr[m]that's pretty cool14/04 18:38
akr[m]lambdabot: not you14/04 18:38
subttleakr[m]: yeah! I'll post more when I get a chance to do some more, it's tough trying to keep up with school work when I just want to be writing code instead :D14/04 22:53
apostolisCan heterogeneous equality be used with cubical enabled? 14/04 23:29

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