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

--- Day changed Tue Feb 20 2018
subttleI see I use `_⊛_` instead of `<*>` but I'm not sure how to get there still20/02 00:06
trikl[m]Did anyone notice that constructors in literate Agda files get extra spaces inserted around them?20/02 00:23
trikl[m]They get put in between tags so they can be referenced. These tags (LaTeX comments) require newlines, and it's these newlines that add an extra space around constructors20/02 00:25
trikl[m]Other `\Agda*{}` commands are all put on the same line until `\AgdaSpace{}`, so they don't have those extra spaces20/02 00:27
trikl[m]It's quite terrible to the view, it is hard to believe that no one has noticed it20/02 00:28
subttleI'm looking into using agda-prelude for the first time now because this is time sensitive but I'm still curious how it's supposed to be done in agda-stdlib20/02 00:39
subttleAnd in the meantime, I just defined liftA2 explicitly for that type, which works but I'm not happy about it :D20/02 00:40

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