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

--- Day changed Tue Feb 14 2017
akrI have BOOM : ∀ {A C : Set} → Empty → C14/02 08:35
akrWhy can't Agda infer what C should be when using BOOM at the "top level" of a function?14/02 08:36
akroh14/02 08:37
akrnevermind, I'm stupid - unused variable A in the type signature14/02 08:38
akrnot sure why it didn't complain where BOOM is defined, though14/02 08:38
rntzakr: well, that's a perfectly legitimate type for something to have14/02 18:05
rntzif C : Set1 instead of Set, the value passed as A might even affect the result of BOOM14/02 18:07
rntz(of course, it won't, but it could)14/02 18:07
akrah you're right I hadn't thought of that14/02 18:13
drdoIs there something that can automatically decidability of equality for defined data?14/02 18:19
drdoInstead of having write a silly function pattern matching on every possibility14/02 18:19
glguyThere exists code that uses Agda's macro system for that. I don't know the actual URL, but I saw it in this channel earlier14/02 18:21
akrpossibly this https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Deriving/Eq.agda14/02 18:29
wedifyi don't know how to fix this error message: http://lpaste.net/35252014/02 20:11
wedifyit seems i have to supply an instance field somehow but i don't know how14/02 20:12
glguywedify: after you write "eqRatio : {a : Set} → Eq (Ratio a)" you'll need to actually provide the definition of eqRatio14/02 21:52
glguyeqRatio = record { ... }, assuming that it's a record14/02 21:53
wedifyglguy: eqRatio is being defined. that's what the _==_ {{eqRatio}} does. going by http://agda.readthedocs.io/en/latest/language/instance-arguments.html that is how instances are defined14/02 22:35
glguyAh, I didn't know about the copattern syntax14/02 22:37
--- Log closed Tue Feb 14 22:46:34 2017
--- Log opened Tue Feb 14 22:46:54 2017
-!- Irssi: #agda: Total of 103 nicks [0 ops, 0 halfops, 0 voices, 103 normal]14/02 22:46
-!- Irssi: Join to #agda was synced in 133 secs14/02 22:49
mietekakr: it should’ve highlighted A in orange14/02 23:42
mietekOr yellow14/02 23:42

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