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

--- Day changed Thu Apr 06 2017
canndrew_when agda gives me a type-checking error like "foo bar blat != jim jom jam in T" is there a way to tell it to normalise both sides of the '!=' as much as possible so I don't have to do it by hand?06/04 03:35
comietekC-u C-u06/04 03:43
comietekas a prefix06/04 03:43
canndrew_thanks, i'll have to look up what that means is vim...06/04 03:50
canndrew_*in vim06/04 03:50
canndrew_Can someone help me with this?...06/04 06:31
canndrew_I'm asking agda what the type of a hole is06/04 06:31
canndrew_the type should be `Ctx`, just a simple type with no arguments or anything, which is defined and in-scope06/04 06:32
canndrew_but instead agda is telling me the type is `_2116 cr ld rd tv i` where cr, ld etc. are all variables that are in-scope in the function06/04 06:32
canndrew_why wouldn't it be able to tell me what the actual type is?06/04 06:33
canndrew_i think it's related to the fact that I have a whole bunch of very-mutually-defined definitions which refer to each other in their types, and I have to be very careful about how I order everything in my file if I want to avoid wierd errors.06/04 06:34
canndrew_speaking of which, will agda ever get better support for mutual definitions so that I don't have to do that?06/04 06:35
mietekcanndrew_: sorry, I was assuming you are interacting with agda using the emacs agda-mode; I don’t know how the same works in vim06/04 09:02
mietekcanndrew_: do you even get to interact at all?06/04 09:02
mietekcanndrew_: mutual definitions have some issues. are you using explicit mutual blocks?06/04 09:03
mietekcanndrew_: in my experience, it’s better to use explicit mutual blocks, and to have the minimum amount necessary inside.06/04 09:03
{AS}canndrew_: consider using spacemacs06/04 11:10
{AS}Which is Agda configured to be vim-like06/04 11:10
bernalexI don't really like spacemacs, but booting it up did convince me that evil was in fact rather pleasant. so spacemacs did push me to finally just start using emacs. and I must say it's mostly a huge improvement from vim. and this is coming from a vim-user for well over a decade.06/04 14:20

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