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

--- Day changed Tue Feb 21 2017
SuprDewdwas there a method in the standard library for getting a colist of all nats in increasing order?21/02 02:04
SuprDewdi.e. Haskell's [0..]21/02 02:04
SuprDewdI feel like I've seen it somewhere, but maybe I'm wrong, as I can't find it now21/02 02:05
SuprDewd(trying to force myself to use the library when I can...)21/02 02:06
wedifyi update agda and now \bn types what looks like a dude standing by a pillar21/02 04:20
wedifyi don't know how to debug/fix this21/02 04:21
wedifyoh. looking at agda-input.el it seems it has changed so now i have to type \bN21/02 04:27
wedifyanyone know why?21/02 04:27
wedifywhat language are those characters anyway?21/02 04:27
mudriwedify: \bn now gives \mathbb n.21/02 12:12
mudriIt was changed to give a regular way to access all of the blackboard bold letters from Unicode.21/02 12:13
mudriwedify: https://github.com/agda/agda/pull/230521/02 12:16
jonsterlingthis is such a good change.21/02 14:58
jonsterlingWOW! It also has blackboard greek. fantastic.21/02 14:59
{AS}Could one not have used MBn before?21/02 15:04
{AS}Oh, I misremembered21/02 15:06
rntzI think I've found a bug in agda's typechecker (not a soundness bug, a "the compiler crashes with an irrefutable pattern-match failure" bug)21/02 15:48
rntzwhere should I report this?21/02 15:49
rntzminimal example: http://sprunge.us/bNQY21/02 15:49
rntzor if you need an example without holes: http://sprunge.us/KcIE21/02 15:51
rntzaha, https://github.com/agda/agda/issues21/02 15:51
rntzok, issue submitted21/02 15:58
wedifyoh i finally figured it out. i decided to try and paste a character into google to see what language it was and it shows up as a blackboard character. so i'm having some emacs font issue21/02 22:11

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