--- Day changed Tue Sep 12 2017
glguykclancy: It probably means that that clause is redundant12/09 00:28
kclancyAccording to the agda customization groups, it means that it is a catchall phrase12/09 00:29
glguyAssuming you're seeing something like this: http://imgur.com/a/0a5AI12/09 00:29
kclancyI think grey is used for redundant clauses12/09 00:29
kclancyit's like that, but white rather than grey12/09 00:31
glguykclancy: You can add {-# CATCHALL #-} above that clause12/09 00:32
subttleJust saw the Agda 2.5.3 and stdlib 0.14 release, woohoo!!!12/09 01:44
--- Log closed Tue Sep 12 02:06:14 2017
--- Log opened Tue Sep 12 02:10:34 2017
-!- Irssi: #agda: Total of 108 nicks [0 ops, 0 halfops, 0 voices, 108 normal]12/09 02:10
-!- Irssi: Join to #agda was synced in 114 secs12/09 02:12
cgraHello, I am trying to understand what rewriting happens behind the scene to make the following code work: http://lpaste.net/358370 12/09 10:30
cgraIs it just Axiom K in the guise of pattern matching? Any feedback is welcome.12/09 10:32
rribeiroHello all! A quick question: I looked at Agda wiki if there's some entry in documentation about memory profiling compiled Agda programs. Is there a way to do it?12/09 23:00

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