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

--- Day changed Fri Feb 17 2017
comietekdrdo: ≉17/02 00:14
comietekdrdo: \~~n17/02 00:14
comietekdrdo: oops, my bad.17/02 00:15
comietekdrdo: I can see ≆ and ≇17/02 00:16
comietekdrdo: the second one is \~=n17/02 00:16
comietekdrdo: both can be found in \eqn17/02 00:16
comietekroconnor: do you want to know if two numbers are equal, and if not, what is the difference?17/02 00:18
comietekroconnor: if you squint, typed de Bruijn indices are numbers. Perhaps take a look at 2.2.4 in https://www.dropbox.com/s/o52bvefwsozg6yh/KellerAltenkirch2010.pdf17/02 00:19
comietekroconnor: it’s probably due to pigworker17/02 00:19
roconnorcomietek: I'm looking to take a goal P n m and turn it into three goals P n n, P (S i + n) n, and P n (S i + n).17/02 01:33
roconnorwhich destructing Ordering n m should end up doing. :D17/02 01:33
roconnorcomietek: oh wow.  I wish I had read this before I proved the Curch-Rosser theorem for the STLC.17/02 01:39
comietekroconnor: got a link to that?17/02 02:43
comietekI assume you mean an Agda development17/02 02:44
comietekWhich I would like to see17/02 02:44
comietekbleh, he quit17/02 02:48
comietekNote to self: thank him for https://github.com/mietek/experiment-floyd-warshall17/02 02:48
drdocomietek: Right, I've found those, but I haven't found the triple ~ with a line through it.17/02 09:18
mietekdrdo: I don’t think there is one in Unicode17/02 10:31
mietekdrdo: you could also see http://shapecatcher.com17/02 10:32
mietekJust found ⧥ in it17/02 10:32
drdoUseful link, thanks :)17/02 10:35
drdoDoesn't work quite that well though :P17/02 10:35
drdoI drew a fairly good \~~ but it shows me clocks instead17/02 10:35
mietekThere may be others; I know of Detexify for LaTeX17/02 10:59
akrI have a situation inside some module M that looks like this: 'module _ {{_ : X}} where open MyRecord {{…}} public […]'17/02 13:35
akrthe issue is that whatever imports M gets infected with the 'open MyRecord […]'17/02 13:35
akris there something I can do to prevent this, other than naming the inner 'module _'?17/02 13:36
mietekakr: have you tried removing "public"?17/02 13:42
akrah, right, that works17/02 13:44
akrthanks17/02 13:44

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