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

--- Day changed Sun Jan 29 2017
subttleHi, quick question if anyone has a moment. I'm working on some code and I receive an error, "Incomplete pattern matching for f. Missing cases: ..." and I then add those cases listed to the end of f (and just leave holes for each on the RHS), and then I receive, "Unreachable clause when checking the definition of f". In general is that supposed to be possible?29/01 03:03
mieteksubttle: have you tried doing a case split? C-c C-c29/01 04:50
subttlemietek: yes, but it ignores all the cases I already had and just gives me all new cases29/01 05:01
mieteksubttle: I would comment out your old code and start from scratch with Agda’s case split29/01 05:01
mieteksubttle: there’s probably an absurd pattern hiding in there29/01 05:02
subttlemietek: yes, for the record I have a working version, I was just trying to rewrite a more concise version :)29/01 05:03
subttlethanks for your help though29/01 05:03
subttleso it is possible then, I think you're right and I'm just missing an absurd pattern somewhere29/01 05:08
subttleexcellent, thanks29/01 05:08

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