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

--- Day changed Thu Mar 16 2017
quchen_Is there a way to ask for the type of the value at the cursor?16/03 12:27
quchen_For example, if I have the cursor on the »4« in »foo : Nat; foo = 4 + 5«, I’d like to get Nat.16/03 12:27
gallaisquchen_: If you put it in a hole (surround it with "{!" and "!}" and reload), C-c C-d will tell you that.16/03 12:41
quchen_gallais: Ah, so it needs a hole. That was my workaround, but I didn’t find it very convenient. Maybe I should write a surround-in-hole plugin :-)16/03 12:42
gallaisIt would indeed be nice to be able to do it for any highlighted expression.16/03 12:43
gallaisYou can maybe open an issue suggesting it? https://github.com/agda/agda/issues16/03 12:43
comietekaugur: when will you be hitting up London?16/03 18:21
comietekOops wrong window16/03 18:21
rntzcan anyone tell me how to use the "inspect idiom" when the thing I want to pattern-match on is just a variable, not a function applied to something?16/03 23:05
rntzbasically, how do I make this typecheck: http://sprunge.us/JUaO16/03 23:09
lpaste_gallais pasted “rntz's Funlist” at http://lpaste.net/35361516/03 23:19
gallaisI don't know how to use inspect but you can with on a telescope so that lookup's type takes the information on length's value in consideration16/03 23:20
rntzhm, interesting.16/03 23:21

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