--- Log closed Sat Apr 01 01:16:45 2017
--- Log opened Sat Apr 01 01:16:52 2017
-!- Irssi: #agda: Total of 127 nicks [0 ops, 0 halfops, 0 voices, 127 normal]01/04 01:16
-!- Irssi: Join to #agda was synced in 135 secs01/04 01:19
vorgangok guysm01/04 20:33
vorgangmy goal is to type-check some program that uses stdlib, but it fails with mysterious error01/04 20:34
vorgangI'll give more detail, maybe someone can help01/04 20:35
vorgangthis is my file FooBar.agda, which I open in emacs: https://pastebin.com/aWqNvxSB01/04 20:38
mietekvorgang: Nat is the module name, ℕ is the type name01/04 20:40
mietekQ : ℕ -> ℕ01/04 20:40
vorganguh, so it's unicode?01/04 20:40
mietekthat’s how the stdlib rolls01/04 20:40
vorganganyway when I press C-c C-l I get this error: https://pastebin.com/uSgrpcFx01/04 20:40
mietekuh…01/04 20:41
vorgangso the error is not in FooBar.agda, but in Empty. agda01/04 20:41
vorgangwhich is why I thought I'd ask here first01/04 20:41
mietekAgda version? stdlib version?01/04 20:41
vorganghang on..01/04 20:41
vorgangagda 2.5.2, stdlib is current from github01/04 20:43
mietekI would suggest not using prerelease Agda until you’re more comfortable with it01/04 20:43
vorgangis agda pre-release, or rather stdlib01/04 20:44
mieteksorry, 2.5.2 is actually the latest release01/04 20:44
mietekbut01/04 20:45
mietekhttps://github.com/agda/agda-stdlib/commit/e8bace203514a2d9c6a4767d1f92f1131518d8f601/04 20:45
mietekthe latest stdlib is probably too new01/04 20:45
mietektry the 0.13 release01/04 20:45
vorgangthat worked! awesome!01/04 20:46
vorganghow do I type ℕ in emacs?01/04 20:47
mietekhttp://agda.readthedocs.io/en/v2.5.2/tools/emacs-mode.html#unicode-input01/04 20:47
mietek\bN by default01/04 20:48
* vorgang bows to mietek 01/04 20:50
mietekyou're welcome01/04 20:50
akr[m]there's a command to find out how to type a character if you already have it in the buffer01/04 20:51
akr[m]but I always forget what it is01/04 20:51
mietekc-U c-X =01/04 20:51
mietekmnemonic: Agda has terrible UX01/04 20:51
akr[m]lol01/04 20:51
mietekdoh, I meant to say, emacs has terrible UX, but, well01/04 20:51
akr[m]it's a bit better in spacemacs ;)01/04 20:52
adamsealso, M-x describe-char, does it and is a bit easier to remember01/04 20:54
mietekif only we had a discoverable method for choosing commands01/04 20:55
mietekwe could call it a menu01/04 20:55
adamsemietek: there is actually "Information about the character at point" in the Agda menu ;)01/04 21:10
akr[m]mietek: I believe that's what spacemacs tries to do01/04 21:15
akr[m]alas, this command is not part of the Agda menu01/04 21:15
akr[m](iirc)01/04 21:15

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