< 1394755244 787386 :vravn!~vravn@syn.rook.sx JOIN :#esoteric < 1394756017 837356 :glogbackup!~glogbacku@192.3.160.190 QUIT :Remote host closed the connection < 1394756190 521457 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :ACTION subtly pokes quintopia < 1394756380 296743 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net JOIN :#esoteric < 1394756396 995855 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover PRIVMSG #esoteric :Taneb, i know a guy who says he made one out of lego < 1394756563 287127 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net JOIN :#esoteric < 1394756670 864355 :FreeFull!~freefull@defocus/sausage-lover PRIVMSG #esoteric :ion: Dreamweaver does that with .cs files < 1394756743 525559 :tromp_!~tromp@69.112.162.42 JOIN :#esoteric < 1394756757 13281 :tromp__!~tromp@ool-4570a22a.dyn.optonline.net JOIN :#esoteric < 1394756761 245454 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net QUIT :Ping timeout: 240 seconds < 1394756929 337217 :tromp_!~tromp@69.112.162.42 QUIT :Ping timeout: 240 seconds < 1394757276 930703 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :hap-pi day < 1394757937 528835 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :joyeux a-pi-versaire! < 1394758179 300291 :b_jonas!~x@russell2.math.bme.hu QUIT :Ping timeout: 240 seconds < 1394758179 515672 :CADD_!uid21876@gateway/web/irccloud.com/x-edgrwodqtazhffel QUIT :Ping timeout: 240 seconds < 1394758202 22220 :myname!~myname@84.200.43.57 QUIT :Ping timeout: 240 seconds < 1394758209 304639 :myname!~myname@84.200.43.57 JOIN :#esoteric < 1394758272 281062 :b_jonas!~x@russell2.math.bme.hu JOIN :#esoteric < 1394758302 189256 :Guest95255!uid21876@gateway/web/irccloud.com/x-rwmurrkabstqhkqf JOIN :#esoteric < 1394758585 251376 :Guest95255!uid21876@gateway/web/irccloud.com/x-rwmurrkabstqhkqf QUIT :Ping timeout: 240 seconds < 1394758710 72822 :Guest95255!uid21876@gateway/web/irccloud.com/x-jiaehmudzxxzlwbf JOIN :#esoteric < 1394758926 648666 :FireFly!~firefly@oftn/member/FireFly QUIT :Excess Flood < 1394758948 949245 :Effilry!~firefly@oftn/member/FireFly JOIN :#esoteric < 1394759044 103772 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover QUIT :Quit: Leaving < 1394759263 337155 :glogbackup!~glogbacku@192.3.160.190 QUIT :Ping timeout: 264 seconds < 1394759329 257338 :lifthrasiir!~lifthrasi@115.68.131.49 QUIT :Ping timeout: 240 seconds < 1394759656 976999 :augur_!~augur@216-164-48-148.c3-0.slvr-ubr1.lnh-slvr.md.cable.rcn.com JOIN :#esoteric < 1394759659 341424 :conehead!~conehead@unaffiliated/conehead QUIT :Quit: Computer has gone to sleep. < 1394759857 183386 :augur!~augur@216-164-48-148.c3-0.slvr-ubr1.lnh-slvr.md.cable.rcn.com QUIT :Ping timeout: 240 seconds < 1394759947 97556 :lifthrasiir!~lifthrasi@115.68.131.49 JOIN :#esoteric < 1394760001 340579 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :ACTION staws Effilry -#--##-- < 1394760033 46369 :tertu_!~quassel@143.44.65.14 JOIN :#esoteric < 1394760038 883463 :luserdroog!636c1b05@gateway/web/freenode/ip.99.108.27.5 JOIN :#esoteric < 1394760048 719616 :tertu!~quassel@143.44.65.14 QUIT :Ping timeout: 240 seconds < 1394760502 9844 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover JOIN :#esoteric < 1394760708 61462 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :oerjan: staws? is that like a Norwegian Mapole? < 1394760805 644774 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :no, that would be stav < 1394760845 705074 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :ACTION is confused < 1394760883 605550 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :what sort of bizarre rettaws is that < 1394760917 470052 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :https://en.wiktionary.org/wiki/stav#Swedish in lack of a norwegian version < 1394760946 921878 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :you might note that Effilry is isomorphic to FireFly hth < 1394761009 389256 :yorick!~yorick@oftn/member/yorick QUIT :Remote host closed the connection < 1394761169 413197 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :ACTION is suddenlilluminated < 1394761190 724393 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :(or is it suddenlightened?) < 1394761207 965741 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :shachaf: thachaf. < 1394761226 745700 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :oerjan: i didn't look at it long enough to see that it wasn't just reversed < 1394761248 217189 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :it would only have taken one letter to see that < 1394761263 410145 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :almost any letter would have worked < 1394761280 862089 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :but still. it's a very weird rettaws, much like a klingon weapon. < 1394761297 209300 :boily!~boily@96.127.201.149 QUIT :Quit: ISOMORPHIC NICHECK < 1394761301 796135 :metasepia!~metasepia@96.127.201.149 QUIT :Remote host closed the connection < 1394762215 316578 :itsy!~digital_w@37.152.198.84 QUIT :Ping timeout: 264 seconds < 1394762217 339681 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover QUIT :Quit: Leaving < 1394762620 136338 :Froox!~Frooxius@cust-101.ktknet.cz QUIT :Read error: Connection reset by peer < 1394762731 357682 :Frooxius!~Frooxius@cust-101.ktknet.cz JOIN :#esoteric < 1394762991 699075 :oerjan!oerjan@sprocket.nvg.ntnu.no QUIT :Quit: Hmm < 1394763260 191586 :Sorella_!~queen@201.80.214.167 NICK :Sorella < 1394763838 838170 :luserdroog!636c1b05@gateway/web/freenode/ip.99.108.27.5 QUIT :Ping timeout: 245 seconds < 1394763871 698915 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :i wonder if there are compilers that will take state machine code like while(1) { switch (state) { ... } } and allocate 'state' in the instruction pointer register, so to speak < 1394763897 967364 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :that is, turn the assignments to 'state' into jumps < 1394764103 278792 :shikhout!~Shikhin@unaffiliated/shikhin JOIN :#esoteric < 1394764303 338848 :shikhin!~Shikhin@unaffiliated/shikhin QUIT :Ping timeout: 264 seconds < 1394764303 543834 :shikhout!~Shikhin@unaffiliated/shikhin NICK :shikhin < 1394765114 947981 :evalj!~jeval@51B6E3DC.dsl.pool.telekom.hu QUIT :Remote host closed the connection < 1394765467 180553 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :print!(" \x1b[36m{:s}\x1b[0m='\x1b[34m{:s}\x1b[0m'", attr.name, attr.value); < 1394765524 841056 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :there are a lot of different languages packed into that one line of code < 1394765911 107490 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu PRIVMSG #esoteric :today i tried to invoke a shell on windows through matlab and i think it gave me VT100 control codes < 1394765914 583421 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu PRIVMSG #esoteric :a disheartening experience < 1394765924 112218 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu PRIVMSG #esoteric :that looked a lot like that string >_> < 1394765937 735859 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :yes < 1394765944 34096 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :those are VT100 control codes, or ECMA-48 codes anyway < 1394765952 451675 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :I don't remember if the actual VT100 had color, probably not < 1394765977 399167 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu PRIVMSG #esoteric :oh. lol i was just shallowly seeing unclosed square brackets < 1394766003 389787 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :it's a good tip-off < 1394766063 539915 :pikhq!~pikhq@2602:100:18b2:fbfb:a60:6eff:fece:493 PRIVMSG #esoteric :ECMA-48 apparently predates the VT100. < 1394766072 271853 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :but not the latest edition, which is from 1991 < 1394766091 820655 :luserdroog!636c1b05@gateway/web/freenode/ip.99.108.27.5 JOIN :#esoteric < 1394766106 192583 :pikhq!~pikhq@2602:100:18b2:fbfb:a60:6eff:fece:493 PRIVMSG #esoteric :Ah sweet, I found the VT100 manual. < 1394766106 618304 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :god bless you ECMA, for making your standards free online and not trying to wring me for every last CHF like those ISO bastards < 1394766117 255724 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :SIPB owns an actual VT100, or is it a VT220 < 1394766128 989872 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :they had it hooked up to a Raspberry Pi, which fit easily within the case < 1394766130 245848 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :it was cute < 1394766157 327078 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :Bike: the two-byte sequenc \x1b [ (i.e. ESCAPE [, i.e. ^[ [) is the Control Sequence Introducer, which begins many of the most important commands < 1394766167 279857 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu PRIVMSG #esoteric :ohhh < 1394766173 374181 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu PRIVMSG #esoteric :i think it printed as like... ~V[ or something < 1394766209 339363 :pikhq!~pikhq@2602:100:18b2:fbfb:a60:6eff:fece:493 PRIVMSG #esoteric :It seems that it did not *support* color, but the VT100 ignores unknown character attributes. < 1394766215 757533 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu PRIVMSG #esoteric :in the end i figured out i could in fact invoke programs directly and just did that and everything went away. huzzah. < 1394766226 640416 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :or rather, it's the 7-bit ASCII representation of CSI. you can also use the character 'CONTROL SEQUENCE INTRODUCER' (U+009B) from the ISO 2022's C1 control code section < 1394766231 136748 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :but mostly people don't < 1394766238 984098 :pikhq!~pikhq@2602:100:18b2:fbfb:a60:6eff:fece:493 PRIVMSG #esoteric :So on a VT100 you don't get color *display*, but the color codes work just fine. < 1394766242 864918 :pikhq!~pikhq@2602:100:18b2:fbfb:a60:6eff:fece:493 PRIVMSG #esoteric :(i.e. "do nothing") < 1394766264 426951 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :presumably on a UTF-8 terminal you would have to write 0xC2 0x9B anyway... < 1394766351 669190 :pikhq!~pikhq@2602:100:18b2:fbfb:a60:6eff:fece:493 PRIVMSG #esoteric :Thankfully all the character attributes are parameters to \ < 1394766363 29946 :pikhq!~pikhq@2602:100:18b2:fbfb:a60:6eff:fece:493 PRIVMSG #esoteric :the "m" sequence. < 1394766378 375920 :pikhq!~pikhq@2602:100:18b2:fbfb:a60:6eff:fece:493 PRIVMSG #esoteric :Which means that it's actually quite simple for a terminal to no-op support the colors. < 1394766385 985801 :pikhq!~pikhq@2602:100:18b2:fbfb:a60:6eff:fece:493 PRIVMSG #esoteric :And apparently the VT100 did just that. < 1394766386 234928 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu PRIVMSG #esoteric :oh as long as i'm complaining i found out that cmd.exe is pretty much terrible < 1394766388 437976 :pikhq!~pikhq@2602:100:18b2:fbfb:a60:6eff:fece:493 PRIVMSG #esoteric :Which is awesome. < 1394766403 578978 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :Bike: yes. you want a better shell (like MSYS bash) and a better terminal emulator (like Mintty) < 1394766418 533648 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu PRIVMSG #esoteric :i invoked a program by quoting the path and it reported the program as having the quote character in it < 1394766445 425417 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu PRIVMSG #esoteric :bash i have, but not a better tty. hoooopefully i won't be using shell enough to want that, but < 1394766447 49995 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :pikhq: I think it's odd that the character telling you what the command is comes at the end, but I suppose it makes sense in an implementation where you're storing to registers as arguments come in, and then you execute < 1394766453 112840 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :which might be how the hardware worked < 1394766456 363353 :pikhq!~pikhq@2602:100:18b2:fbfb:a60:6eff:fece:493 PRIVMSG #esoteric :Probably. < 1394766471 491207 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu PRIVMSG #esoteric :of course, msys doesn't have man pages :( oh well < 1394766549 713611 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu PRIVMSG #esoteric :also: does anyone know what the hell git rev-parse is < 1394766608 571854 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu PRIVMSG #esoteric :"A similar notation r1...r2 is called symmetric difference of r1 and r2 and is defined as r1 r2 --not $(git merge-base --all r1 r2). " pretty sure i'm out of my league here < 1394766647 824619 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu PRIVMSG #esoteric :"Note that .. would mean HEAD..HEAD which is an empty range that is both reachable and unreachable from HEAD." < 1394766649 715291 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :Bike: it describes the syntax you can use to name git objects, mainly commits < 1394766675 907161 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :the actual rev-parse command is meant for use from scripts < 1394766686 58999 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :but many of the user-facing commands accept the same syntax < 1394766693 769831 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu PRIVMSG #esoteric :getting the last commit object was both easier (since it's just "git rev-parse HEAD") and harder (since i have no idea wtf) than i thought it would be < 1394766697 58340 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :(because they are shell scripts that invoke rev-parse, or they used to be) < 1394766838 863080 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu PRIVMSG #esoteric :maybe someday i will have a job where i have to learn git because everyone else uses it instead of just me < 1394768917 804367 :conehead!~conehead@unaffiliated/conehead JOIN :#esoteric < 1394769171 201880 :nisstyre!~yourstrul@oftn/member/Nisstyre JOIN :#esoteric < 1394769419 362647 :Sorella!~queen@201.80.214.167 QUIT :Quit: It is tiem! < 1394769537 111961 :tertu_!~quassel@143.44.65.14 QUIT :Ping timeout: 255 seconds < 1394769562 197701 :tertu!~quassel@143.44.65.14 JOIN :#esoteric < 1394769649 247009 :nisstyre!~yourstrul@oftn/member/Nisstyre QUIT :Ping timeout: 240 seconds < 1394769660 385109 :password2!~password@197.78.153.55 JOIN :#esoteric < 1394769929 361355 :conehead!~conehead@unaffiliated/conehead QUIT :Quit: Computer has gone to sleep. < 1394770282 377247 :tromp__!~tromp@ool-4570a22a.dyn.optonline.net QUIT :Remote host closed the connection < 1394770316 299972 :tromp_!~tromp@ool-4570a22a.dyn.optonline.net JOIN :#esoteric < 1394770374 90405 :glogbackup!~glogbacku@192.3.160.190 QUIT :Ping timeout: 255 seconds < 1394770532 373689 :tromp__!~tromp@ool-4570a22a.dyn.optonline.net JOIN :#esoteric < 1394770546 104196 :tromp_!~tromp@ool-4570a22a.dyn.optonline.net QUIT :Read error: Connection reset by peer < 1394770550 200881 :tromp__!~tromp@ool-4570a22a.dyn.optonline.net QUIT :Remote host closed the connection < 1394770862 70972 :tromp_!~tromp@ool-4570a22a.dyn.optonline.net JOIN :#esoteric < 1394771260 185210 :tromp_!~tromp@ool-4570a22a.dyn.optonline.net QUIT :Read error: Connection reset by peer < 1394771287 371435 :glogbackup!~glogbacku@192.3.160.190 QUIT :Ping timeout: 264 seconds < 1394771440 722634 :conehead!~conehead@unaffiliated/conehead JOIN :#esoteric < 1394771967 46331 :glogbackup!~glogbacku@192.3.160.190 QUIT :Ping timeout: 255 seconds < 1394772507 32223 :tertu!~quassel@143.44.65.14 QUIT :Ping timeout: 255 seconds < 1394772568 979082 :tertu!~quassel@143.44.65.14 JOIN :#esoteric < 1394775033 59084 :limitless23!~limitless@72.11.34.197 JOIN :#esoteric < 1394775075 774836 :limitless23!~limitless@72.11.34.197 QUIT :Client Quit < 1394775109 50121 :limitless23!~limitless@72.11.34.197 JOIN :#esoteric < 1394775137 945274 :limitless23!~limitless@72.11.34.197 PRIVMSG #esoteric :hello < 1394775330 939352 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :`relcome limitless23 < 1394775332 111401 :HackEgo!~HackEgo@162.248.166.242 PRIVMSG #esoteric :​09limitless23: 02Welcome 06to 13the 04international 07hub 08for 09esoteric 02programming 06language 13design 04and 07deployment! 08For 09more 02information, 06check 13out 04our 07wiki: 08. 09(For 02the 06other 13kind 04of 07esoterica, 08try 09#esoteric 02on 06irc.dal.net.) < 1394775337 225374 :password2!~password@197.78.153.55 QUIT :Ping timeout: 240 seconds < 1394776569 995197 :oklopol!~oklopol@dyn60-339.yok.fi JOIN :#esoteric < 1394776956 54436 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :> let welcome = "Hi" in welcome < 1394776956 165105 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :04"Hi" : 12String < 1394776957 388441 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : "Hi" < 1394776983 719822 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :I'm sure there's some way to make idris-ircslave be more colorful < 1394777039 638495 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :> the (t : Type ** t) (String ** "Hello") < 1394777039 748941 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :04(12String 04** 04"Hello"04) : 12(13t 12** 13t12) < 1394777041 189314 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : Not in scope: `the'Not in scope: data constructor `Type'Not in scope: data c... < 1394777242 795573 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :> the (t1 ** t1) ((t3 ** t3) ** (the (t2 ** t2) (String ** "Hello"))) < 1394777243 17450 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :04(12(13t3 12** 13t312) 04** 04(12String 04** 04"Hello"04)04) : 12(13t1 12** 13t112) < 1394777244 578580 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : Not in scope: `the'Not in scope: `t1' < 1394777244 800202 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : Perhaps you meant one of these: < 1394777244 855024 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : `t' (imported from Debug.SimpleReflect), < 1394777244 855215 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : `to' (imported from Control.Lens), < 1394777244 855307 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : `_1' (imported from Control.Lens)Not in scope: `t1' < 1394777293 177434 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :I really like that both bots respond < 1394777307 516596 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :also I wish lambdabot would come back to ##crypto < 1394777338 657879 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :I can add a spalsh of green < 1394777340 434999 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :> :t the (t1 ** t1) ((t3 ** t3) ** (the (t2 ** t2) (String ** "Hello"))) < 1394777340 768103 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :09the 12(13t1 12** 13t112) 04(12(13t3 12** 13t312) 04** 09the 12(13t2 12** 13t212) 04(12String 04** 04"Hello"04)04) : 12(13t1 12** 13t112) < 1394777342 101376 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : :1:1: parse error on input `:' < 1394777377 364456 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Melvar: What colors am I missing? < 1394777409 167835 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :is ** a tuple constructor? < 1394777416 589485 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :It's a dependent pair constructor < 1394777426 949554 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Well, not an actual constructor, it's syntax sugar < 1394777436 528437 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :> :t Exists < 1394777436 638436 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :12Exists : (13a : 12Type) -> (13a -> 12Type) -> 12Type < 1394777437 527927 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : :1:1: parse error on input `:' < 1394777442 404489 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :> :t Ex_intro < 1394777443 351680 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : :1:1: parse error on input `:' < 1394777443 682378 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :04Ex_intro : (13x : 13a) -> (13P 13x) -> 12Exists 13a 13P < 1394777470 244586 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :The typical example is < 1394777509 814463 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :> the (n : Nat ** Vect n String) (5, ["a", "b", "c", "d", "e"]) < 1394777509 924940 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :Can't unify < 1394777510 35693 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric : 12(13A12, 13B12) < 1394777510 90371 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :with < 1394777510 90507 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric : 12(13n 12** 12Vect 13n 12String12) < 1394777510 90597 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :Specifically:14↵… < 1394777510 842587 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : Not in scope: `the'Not in scope: data constructor `Nat'Not in scope: data co... < 1394777525 279979 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :> the (n : Nat ** Vect n String) (5 ** ["a", "b", "c", "d", "e"]) < 1394777525 499476 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :04(045 04** 04[04"a"04, 04"b"04, 04"c"04, 04"d"04, 04"e"04]04) : 12(13n 12** 12Vect 13n 12String12) < 1394777526 537100 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : Not in scope: `the'Not in scope: data constructor `Nat'Not in scope: data co... < 1394777566 687802 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :I don't fully understand the implications of when this is useful, but apparently filtering vects returns a dependent tuple instead of just a resulting vector < 1394777590 177665 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :I guess when you want a component of the type to be readable at runtime? < 1394777722 752517 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :i ascended nethack today < 1394777725 425808 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :why did i even play < 1394777742 281583 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :and what's "the"? < 1394777746 250543 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :i've played three games over the past few days. i think i haven't played any others in over a year < 1394777752 295070 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Vect.idr#L285 < 1394777755 934002 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :the is like id with an explicit type argument < 1394777759 907098 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :ok < 1394777761 195568 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :it's used kind of like :: in haskell < 1394777773 166700 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :the : (a : Type) -> a -> a < 1394777777 232579 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :the Int 5 < 1394777792 91843 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :yeah < 1394777820 854010 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :I saw someone use the infix earlier. Int `the` 5 kind of reads backwards < 1394777880 129319 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :(p ** Vect p a) gets inferred to (p : Nat ** Vect p a) ? < 1394777903 503421 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :I believe so < 1394778050 532988 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Hmm, I don't see examples in the Vect prelude lib, but... maybe you could pattern match on the first part of it to know what you can do with the second? < 1394778078 191167 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :makes sense < 1394778094 913612 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :Conan `the` "Barbarian" < 1394778125 972408 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :one thing I find hard about dependent language syntax is that there's usually a way to leave off either side of (x : t) and it's hard to keep them straight even if I theoreticall understand what's going on < 1394778403 665358 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :"Hello Sir/Madam, I'm Thomas Clark and I'll like to purchase Propane" < 1394778416 573925 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :i get some weird spam < 1394778459 338491 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu PRIVMSG #esoteric :hello kmc, i would like to purchase n-decane to go with my chain link fences, < 1394778566 35655 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :ACTION wants antipane < 1394778603 682225 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :I got spam for Computeroxy -- "an academic website exclusively dedicated to academic careers in schools of electrical and electronic engineering and computer science in Europe, Oceania and the Middle East" -- the other day. < 1394778617 125498 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :"I found this academic website interesting and I think you would enjoy it too." < 1394778654 407535 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :Yeah, I'm sure you thought about me personally, "Mark, Lecturer in Computer Science", the guy sending mail to "undisclosed-recipients:;". < 1394778898 38636 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :"This product is property of Lenovo and may not be distributed outside Lenovo" < 1394778912 967933 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Came with my Lenovo laptop < 1394779001 570070 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :haha < 1394779003 186671 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :what is it? < 1394779009 798536 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :the product i mean < 1394779076 348035 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Some VBScript to... do something < 1394779092 21645 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Not entirely sure what. Something to do with setting up a user guide on Metro, I think < 1394779103 677746 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :"Installing user guide for Support Metro app on Windows 8" < 1394779395 366357 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :ACTION 's brain breaks a bit < 1394779396 264260 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :> let f = (\x => if x == "a" then String else Int) in the (a : String ** f a) ("a" ** "foo") < 1394779396 517410 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :04(04"a" 04** 04"foo"04) : 12(13a 12** 09boolElim (09intToBool (09prim__eqString 13a 04"a")) (04Delay 12String) (04Delay 12Int)12) < 1394779397 479136 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : :1:13: parse error on input `=>' < 1394779515 768515 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :> let f = (\x => if x == "a" then String else Int) in the (a : String ** f a) ("a" ** 5) < 1394779515 989219 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :Can't resolve type class 12Num (09boolElim (09intToBool (09prim__eqString 04"a" 04"a")) (04Delay 12String) (04Delay 12Int)) < 1394779516 801529 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : :1:13: parse error on input `=>' < 1394779533 467165 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :> let f = (\x => if x == "a" then String else Int) in the (a : String ** f a) ("b" ** 5) < 1394779533 687583 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :04(04"b" 04** 04504) : 12(13a 12** 09boolElim (09intToBool (09prim__eqString 13a 04"a")) (04Delay 12String) (04Delay 12Int)12) < 1394779534 680221 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : :1:13: parse error on input `=>' < 1394779542 388670 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :> let f = (\x => if x == "a" then String else Int) in the (a : String ** f a) ("b" ** "5") < 1394779543 425184 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :Can't unify < 1394779543 482782 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric : 12String < 1394779543 482930 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :with < 1394779543 483022 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric : (\13a => 09boolElim (09intToBool (09prim__eqString 13a 04"a")) (04Delay 12String) (04Delay 12Int)) 04"b" < 1394779543 483113 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :Specifically:14↵… < 1394779543 539654 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : :1:13: parse error on input `=>' < 1394779546 320000 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :ACTION stops < 1394779559 67245 :Slereahphone!~slereahph@80.10.159.144 JOIN :#esoteric < 1394779566 664731 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Slereahphone: you just missed the fun < 1394780075 409675 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :we put the fun in dependently-typed functional programming < 1394780207 152674 :Slereahphone!~slereahph@80.10.159.144 PRIVMSG #esoteric :It can't be that fun because < 1394780215 491739 :Slereahphone!~slereahph@80.10.159.144 PRIVMSG #esoteric :I don't know what it means < 1394780478 234929 :luserdroog!636c1b05@gateway/web/freenode/ip.99.108.27.5 PRIVMSG #esoteric :translated the Lukasiewicz logic interpreter to C. https://gist.github.com/luser-dr00g/9542998 < 1394780544 159619 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :> the Type Type < 1394780544 421261 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :12Type : 12Type < 1394780545 296331 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : Not in scope: `the'Not in scope: data constructor `Type'Not in scope: data c... < 1394780687 990702 :^v!~notnot^v@c-71-238-153-166.hsd1.mi.comcast.net QUIT :Quit: Leaving < 1394781666 393619 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :Is the type type the typest of the types? < 1394781718 447778 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Idris has a cumulative universe thingy and then hides it < 1394781748 422285 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :So the type of Type is Type 1, the type of Type 1 is Type 2... but Type is also a Type 2, and small types are also Type 2s, and Type 3s, and Type 4s < 1394781760 572297 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :And somehow this lets Idris hide the entire hierarchy from the user < 1394781792 928565 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :So I guess Type becomes whatever Type in the hierarchy is needed in context < 1394781876 846800 :limitless23!~limitless@72.11.34.197 QUIT :Quit: Leaving < 1394781879 859405 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu PRIVMSG #esoteric :> the (Type 17) Type < 1394781879 914418 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :(input):1:11:12Type does not have a function type (12Type) < 1394781880 898090 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : Not in scope: `the'Not in scope: data constructor `Type'Not in scope: data c... < 1394781888 494451 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu PRIVMSG #esoteric :well what's the point then!! < 1394781944 823230 :FreeFull!~freefull@defocus/sausage-lover QUIT : < 1394782081 408849 :atehwa!atehwa@aulis.sange.fi QUIT :Ping timeout: 265 seconds < 1394782091 826879 :Effilry!~firefly@oftn/member/FireFly NICK :FireFly < 1394782092 31790 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :You can't actually write Type 1 < 1394782093 787962 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :etc. < 1394782108 137758 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :The only place it's ever visible, as far as I understand, is < 1394782111 786360 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :> :t Type < 1394782112 30096 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :12Type : 12Type 1 < 1394782112 957790 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : :1:1: parse error on input `:' < 1394782129 375920 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu PRIVMSG #esoteric :well what if i want to talk about specifically the type of Int or w/e < 1394782177 362951 :atehwa!atehwa@aulis.sange.fi JOIN :#esoteric < 1394782223 412207 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Good question. Not sure you can < 1394782285 281236 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu PRIVMSG #esoteric :> :t Int < 1394782285 337197 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :12Int : 12Type < 1394782286 324338 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : :1:1: parse error on input `:' < 1394782557 520636 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :help < 1394782564 813182 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :trackpad acting up < 1394782612 744392 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Fixed < 1394782616 475202 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Thanks to a mouse < 1394783711 326765 :Slereahphone!~slereahph@80.10.159.144 QUIT :Remote host closed the connection < 1394783791 223347 :Slereahphone!~slereahph@80.10.159.144 JOIN :#esoteric < 1394784139 954355 :Slereahphone_!~slereahph@80.10.159.144 JOIN :#esoteric < 1394784140 279274 :Slereahphone!~slereahph@80.10.159.144 QUIT :Remote host closed the connection < 1394784141 579801 :Slereahphone_!~slereahph@80.10.159.144 NICK :Slereahphone < 1394784358 530178 :Slereahphone!~slereahph@80.10.159.144 QUIT :Remote host closed the connection < 1394784363 275039 :Slereahphone_!~slereahph@80.10.159.144 JOIN :#esoteric < 1394785702 266880 :shikhout!~Shikhin@unaffiliated/shikhin JOIN :#esoteric < 1394785903 305349 :shikhin!~Shikhin@unaffiliated/shikhin QUIT :Ping timeout: 264 seconds < 1394785904 525628 :shikhout!~Shikhin@unaffiliated/shikhin NICK :shikhin < 1394786404 155699 :Slereahphone_!~slereahph@80.10.159.144 PRIVMSG #esoteric :What's the size of a tab in console mode < 1394786421 720168 :Slereahphone_!~slereahph@80.10.159.144 PRIVMSG #esoteric :In character spaces < 1394787411 165832 :tertu!~quassel@143.44.65.14 QUIT :Ping timeout: 255 seconds < 1394787855 153480 :FireFly!~firefly@oftn/member/FireFly PRIVMSG #esoteric :up to the next tabstop, as defined by tabs(1) < 1394787863 148957 :FireFly!~firefly@oftn/member/FireFly PRIVMSG #esoteric :defaults to every eighth column < 1394787875 146499 :FireFly!~firefly@oftn/member/FireFly PRIVMSG #esoteric :if by console mode you mean in a terminal emulator < 1394788112 310617 :Slereahphone_!~slereahph@80.10.159.144 QUIT :Quit: Colloquy for iPhone - http://colloquy.mobi < 1394788325 145948 :Slereahphone!~slereahph@80.10.159.144 JOIN :#esoteric < 1394788639 302085 :MindlessDrone!~MindlessD@unaffiliated/mindlessdrone JOIN :#esoteric < 1394789056 559988 :Jafet!~jafet@unaffiliated/jafet PRIVMSG #esoteric :What about apathy mode < 1394790225 745741 :conehead!~conehead@unaffiliated/conehead QUIT :Quit: Computer has gone to sleep. < 1394790498 970387 :Sellyme!~Sellyme@irc.sellyme.com QUIT :Excess Flood < 1394790535 818674 :Sellyme!~Sellyme@fluttershy.is.bestpony.tk JOIN :#esoteric < 1394790697 289446 :glogbackup!~glogbacku@192.3.160.190 QUIT :Ping timeout: 240 seconds < 1394792038 274471 :boily!~boily@96.127.201.149 JOIN :#esoteric < 1394794990 294050 :boily!~boily@96.127.201.149 QUIT :Quit: PENTASYLLABIC CHICKEN < 1394795498 503642 :Melvar!~melvar@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :Sgeo_, Bike: Use ( as a prefix in here so it doesn’t clash with lambdabot. < 1394795582 372258 :Jafet!~jafet@unaffiliated/jafet PRIVMSG #esoteric :“In September 1943, Iran declared war on Germany, thus qualifying for membership in the United Nations.” < 1394795700 868537 :Melvar!~melvar@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :Sgeo_, Bike: The way the Type hierarchy works is that it builds up a digraph of universe ordering, and checks at the end that it’s consistent (i.e. cycle-free), IIUC. < 1394795960 190516 :glogbackup!~glogbacku@192.3.160.190 QUIT :Read error: Connection reset by peer < 1394796313 293754 :Slereahphone!~slereahph@80.10.159.144 QUIT :Ping timeout: 240 seconds < 1394796474 141558 :TodPunk!Tod@50-198-177-186-static.hfc.comcastbusiness.net QUIT :Ping timeout: 245 seconds < 1394797130 95835 :glogbackup!~glogbacku@192.3.160.190 QUIT :Ping timeout: 252 seconds < 1394797418 319228 :glogbackup!~glogbacku@192.3.160.190 QUIT :Ping timeout: 240 seconds < 1394798505 247760 :Sorella!~queen@oftn/member/Sorella JOIN :#esoteric < 1394798578 334799 :glogbackup!~glogbacku@192.3.160.190 QUIT :Ping timeout: 240 seconds < 1394798623 448815 :spiette!~spiette@mtl.savoirfairelinux.net QUIT :Remote host closed the connection < 1394799391 47351 :Taneb!~Taneb@runciman.hacksoc.org PRIVMSG #esoteric :> 47/15 < 1394799391 603366 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :043.1333333333333333 : 12Float < 1394799392 77649 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : 3.1333333333333333 < 1394799577 283482 :glogbackup!~glogbacku@192.3.160.190 QUIT :Ping timeout: 240 seconds < 1394800223 301589 :password2!~password@197.78.163.189 JOIN :#esoteric < 1394800589 831277 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net QUIT :Read error: Connection reset by peer < 1394801108 725145 :glogbackup!~glogbacku@192.3.160.190 QUIT :Ping timeout: 240 seconds < 1394801136 171383 :oerjan!oerjan@sprocket.nvg.ntnu.no JOIN :#esoteric < 1394801436 60351 :TodPunk!Tod@50-198-177-186-static.hfc.comcastbusiness.net JOIN :#esoteric < 1394801665 262471 :glogbackup!~glogbacku@192.3.160.190 QUIT :Ping timeout: 240 seconds < 1394802027 853861 :glogbackup!~glogbacku@192.3.160.190 QUIT :Remote host closed the connection < 1394802045 453868 :quintopia!~quintopia@unaffiliated/quintopia PRIVMSG #esoteric :help my googlebubble thinks i want hockey scores < 1394802120 674627 :MindlessDrone!~MindlessD@unaffiliated/mindlessdrone QUIT :Read error: Operation timed out < 1394802217 725402 :MindlessDrone!~MindlessD@unaffiliated/mindlessdrone JOIN :#esoteric < 1394802263 434157 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :quintopia: i'm sorry you're on thin ice there < 1394802304 839051 :quintopia!~quintopia@unaffiliated/quintopia PRIVMSG #esoteric :ug < 1394802317 891763 :quintopia!~quintopia@unaffiliated/quintopia PRIVMSG #esoteric :hand me your frying pan please < 1394802357 226806 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :managed to edit haskellwiki this time. turns out their fancy layout doesn't work with a non-full-screen browser. < 1394802378 718338 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :since when do i have a frying pan < 1394802384 572063 :quintopia!~quintopia@unaffiliated/quintopia PRIVMSG #esoteric :sounds compatible < 1394802426 642406 :Melvar!~melvar@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :Fullscreen? Not just requiring a certain window size? < 1394802427 938836 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :as in, the edit form got hid under some of the other stuff until i maximized < 1394802474 523822 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :Melvar: well it doesn't work with my _usual_ window size, which is a little less than full screen because i like to be able to glimpse what's happening in irc. < 1394802500 742850 :Melvar!~melvar@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :ACTION has two monitors for that purpose. < 1394802557 190168 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :well this is a laptop, on my lap. < 1394802577 219654 :glogbackup!~glogbacku@192.3.160.190 QUIT :Ping timeout: 240 seconds < 1394802577 971166 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :i don't think you usually have a two-monitor laptop setup. < 1394802580 73957 :Melvar!~melvar@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :ACTION nods. < 1394802623 935498 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :(technically it cannot be a laptop because the manual warns against burns if you put it on your lap. hasn't been a problem though, it's cooler than my previous one.) < 1394802720 316675 :MindlessDrone!~MindlessD@unaffiliated/mindlessdrone QUIT :Read error: Connection reset by peer < 1394802720 676726 :elliott_!~elliott@unaffiliated/elliott PRIVMSG #esoteric :I thought infertility was the usual risk. < 1394802738 377419 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :oh. well i have no plans to breed. < 1394802755 719932 :Melvar!~melvar@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :I’m pretty sure that’s just temporary though. < 1394802760 786117 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :(i actively dislike babies anyway) < 1394802772 982583 :Jafet!~jafet@unaffiliated/jafet PRIVMSG #esoteric :http://mashable.com/category/dual-screen-laptop < 1394802790 19484 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :Melvar: i'm 43, how long is temporary? < 1394802813 659176 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :oh you mean the infertility. < 1394802833 356897 :Melvar!~melvar@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :I meant the infertility, yes. < 1394802846 217885 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :good, good < 1394802888 392651 :Taneb!~Taneb@runciman.hacksoc.org PRIVMSG #esoteric :oerjan, you mean there's never going to be any wild oerjanlings? < 1394802905 646973 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :Taneb: quite unlikely. < 1394803664 732568 :HackEgo!~HackEgo@162.248.166.242 QUIT :Ping timeout: 264 seconds < 1394803970 421479 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :fungot: be careful, someone is picking off bots again < 1394803970 515279 :fungot!fis@eos.zem.fi PRIVMSG #esoteric :oerjan: " and the creator of of yours, you would let the woman with years of combat, probably against a paladin" miko, i have my eye! < 1394804236 755146 :Taneb!~Taneb@runciman.hacksoc.org PRIVMSG #esoteric :I ought to get dressed at some point < 1394804256 433056 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :you know, _someone_ could have told Sgeo idris-ircslave now supports the ( prefix. < 1394804294 88209 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :@tell Sgeo please use idris-ircslave's new ( prefix hth < 1394804294 303447 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric :Consider it noted. < 1394804314 885684 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :@tell Sgeo_ please use idris-ircslave's new ( prefix hth < 1394804315 101364 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric :Consider it noted. < 1394804445 344506 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :ACTION barely resisted adding "OR DIE" in there. < 1394804470 573769 :Taneb!~Taneb@runciman.hacksoc.org PRIVMSG #esoteric :Is there a nice way to compute the Thue-Morse sequence on a Turing machine < 1394804487 862560 :Taneb!~Taneb@runciman.hacksoc.org PRIVMSG #esoteric :(I'm so glad this channel exists so I can ask questions like that) < 1394804498 216206 :glogbackup!~glogbacku@192.3.160.190 QUIT :Ping timeout: 240 seconds < 1394804516 700154 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :well depends what you mean, since turing machines technically have finite output if they ever halt < 1394804554 529619 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :you could certainly manage to fill up the tape with it without halting. < 1394804581 256866 :Taneb!~Taneb@runciman.hacksoc.org PRIVMSG #esoteric :oerjan, I would like to continuously write the Thue-Morse sequence to the tape < 1394804658 662452 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :four cell values, call them 0,1,A,B < 1394804703 116042 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :start by putting 0B on the tape, position yourself just after the B < 1394804767 583602 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :(1) seek left to a 0 or 1. go one step right. < 1394804813 3408 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :(2) turn the A or B that is there into 0 or 1, respectively. remember what it was. seek till end of tape. < 1394804845 373887 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :(3A) put AB on end of tape, go to 1 < 1394804857 373799 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :(3B) put BA on end of tape, go to 1 < 1394804866 62497 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :Taneb: simple enough? < 1394804921 977376 :Taneb!~Taneb@runciman.hacksoc.org PRIVMSG #esoteric :Yes < 1394804935 267513 :Slereahphone!~slereahph@193.253.170.149 JOIN :#esoteric < 1394804940 33323 :Taneb!~Taneb@runciman.hacksoc.org PRIVMSG #esoteric :Thank you < 1394805059 746398 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :you're welcome < 1394805242 94761 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :small adjustment, the "position yourself just after the B" could more efficiently be on the 0. < 1394806734 563315 :glogbackup!~glogbacku@192.3.160.190 QUIT :Ping timeout: 252 seconds < 1394807030 279106 :nisstyre!~yourstrul@oftn/member/Nisstyre JOIN :#esoteric < 1394807338 705072 :shikhout!~Shikhin@unaffiliated/shikhin JOIN :#esoteric < 1394807520 907961 :shikhin!~Shikhin@unaffiliated/shikhin QUIT :Ping timeout: 255 seconds < 1394807522 410882 :shikhout!~Shikhin@unaffiliated/shikhin NICK :shikhin < 1394809075 527645 :nooodl!~nooodl@91.177.69.110 JOIN :#esoteric < 1394809109 596716 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :oerjan: Do they sell two-monitor laptops for people with two heads? < 1394809130 993008 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :Oh, I see Jafet already answered that. < 1394809163 32712 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :ooh i missed that < 1394809186 161485 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :Well, it doesn't exactly mention two-headed people. < 1394809195 495611 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :But I'm sure it's implied. < 1394809216 839956 :Jafet!~jafet@unaffiliated/jafet PRIVMSG #esoteric :I imagine those laptops are marketed beyond the very limited dicephalic demographic. < 1394809222 683065 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :the top picture seems broken < 1394809322 397934 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :fizzie: the Beeblebrox market segment is a bit small, methinks. < 1394809327 387119 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :i think google mustn't have quite the right picture of me, it's showing me an ad for farming equipment. < 1394809377 455275 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :ACTION is late and redundant, as usual. *sigh* < 1394809396 299968 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :int-e: well it's easy to be redundant when you have two heads < 1394809669 771675 :spiette!~spiette@mtl.savoirfairelinux.net JOIN :#esoteric < 1394809681 261027 :glogbackup!~glogbacku@192.3.160.190 QUIT :Ping timeout: 240 seconds < 1394809833 745491 :^v!~notnot^v@c-71-238-153-166.hsd1.mi.comcast.net JOIN :#esoteric < 1394810644 790566 :Slereahphone!~slereahph@193.253.170.149 QUIT :Remote host closed the connection < 1394810864 396988 :AnotherTest!~turingcom@94-224-16-121.access.telenet.be JOIN :#esoteric < 1394811157 841784 :glogbackup!~glogbacku@192.3.160.190 QUIT :Ping timeout: 252 seconds < 1394811193 270190 :password2!~password@197.78.163.189 QUIT :Ping timeout: 240 seconds < 1394811288 246350 :chaiomanot!~chaiomano@75-121-39-142.dyn.centurytel.net JOIN :#esoteric < 1394811544 289052 :password2!~password@197.78.163.189 JOIN :#esoteric < 1394811773 238749 :Slereahphone!~slereahph@193.253.170.149 JOIN :#esoteric < 1394812115 148262 :nooodl!~nooodl@91.177.69.110 QUIT :Ping timeout: 252 seconds < 1394812192 717421 :erdic!erdic@unaffiliated/motley QUIT :Remote host closed the connection < 1394812224 125002 :erdic!erdic@unaffiliated/motley JOIN :#esoteric < 1394812313 189663 :Slereahphone!~slereahph@193.253.170.149 QUIT :Ping timeout: 253 seconds < 1394812494 143159 :Slereahphone!~slereahph@193.253.170.149 JOIN :#esoteric < 1394812847 656555 :shikhout!~Shikhin@unaffiliated/shikhin JOIN :#esoteric < 1394812974 869443 :shikhin!~Shikhin@unaffiliated/shikhin QUIT :Ping timeout: 255 seconds < 1394812975 835008 :shikhout!~Shikhin@unaffiliated/shikhin NICK :shikhin < 1394813586 816645 :nooodl!~nooodl@62.205.81.193 JOIN :#esoteric < 1394814549 931979 :glogbackup!~glogbacku@192.3.160.190 QUIT :Remote host closed the connection < 1394815373 822580 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu PRIVMSG #esoteric :http://www.theguardian.com/technology/2014/mar/14/mtgox-knowingly-traded-non-existent-bitcoins-for-two-weeks-filing-shows ha ha < 1394815561 916280 :oerjan!oerjan@sprocket.nvg.ntnu.no QUIT :Quit: Fnord < 1394818735 740981 :nisstyre!~yourstrul@oftn/member/Nisstyre QUIT :Read error: Operation timed out < 1394819158 368410 :password2!~password@197.78.163.189 QUIT :Ping timeout: 240 seconds < 1394819354 541497 :Sellyme!~Sellyme@fluttershy.is.bestpony.tk QUIT :Excess Flood < 1394819455 785147 :Sellyme!~Sellyme@irc.sellyme.com JOIN :#esoteric < 1394820393 375425 :Slereah__!~jackal@176.222.51.233 JOIN :#esoteric < 1394820614 130578 :^v!~notnot^v@c-71-238-153-166.hsd1.mi.comcast.net QUIT :Read error: Connection reset by peer < 1394820639 758070 :^v!~notnot^v@c-71-238-153-166.hsd1.mi.comcast.net JOIN :#esoteric < 1394820976 770847 :conehead!~conehead@unaffiliated/conehead JOIN :#esoteric < 1394821328 943373 :FreeFull!~freefull@host-92-24-45-223.ppp.as43234.net JOIN :#esoteric < 1394821333 484207 :FreeFull!~freefull@host-92-24-45-223.ppp.as43234.net QUIT :Changing host < 1394821333 539658 :FreeFull!~freefull@defocus/sausage-lover JOIN :#esoteric < 1394822304 85215 :luserdroog!636c1b05@gateway/web/freenode/ip.99.108.27.5 PRIVMSG #esoteric :For the dual-screen laptop, it would be nice to reduce the width of the framing down the middle. < 1394823064 674550 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :Lenovo sold a W-series ThinkPad with a second smaller screen that pops out the side of the first one < 1394823082 611972 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :it also had a Wacom drawing tablet in the wrist rest, as well as a color calibration sensor for the main screen < 1394823443 566857 :olsner!~salparot@c83-252-203-32.bredband.comhem.se PRIVMSG #esoteric :sounds nice, but slightly crazy < 1394824390 510981 :nisstyre!~yourstrul@oftn/member/Nisstyre JOIN :#esoteric < 1394824928 292890 :nisstyre!~yourstrul@oftn/member/Nisstyre QUIT :Ping timeout: 240 seconds < 1394826804 827845 :Bike!~Glossina@gannon-wless-gw.resnet.wsu.edu QUIT :Quit: later < 1394827673 685082 :password2!~password@197.78.152.2 JOIN :#esoteric < 1394827904 850457 :password2!~password@197.78.152.2 QUIT :Client Quit < 1394827933 346919 :password2!~password@197.78.152.2 JOIN :#esoteric < 1394827951 971412 :password2!~password@197.78.152.2 QUIT :Client Quit < 1394828049 273236 :password2!~password@197.78.152.2 JOIN :#esoteric < 1394828378 282272 :AnotherTest!~turingcom@94-224-16-121.access.telenet.be QUIT :Ping timeout: 240 seconds < 1394828514 39133 :password2_!~password@197.78.152.2 JOIN :#esoteric < 1394828584 903784 :erdic!erdic@unaffiliated/motley QUIT :Remote host closed the connection < 1394828612 866195 :erdic!erdic@unaffiliated/motley JOIN :#esoteric < 1394828905 280187 :nooodl!~nooodl@62.205.81.193 QUIT :Ping timeout: 240 seconds < 1394829107 908599 :^v!~notnot^v@c-71-238-153-166.hsd1.mi.comcast.net QUIT :Quit: Leaving < 1394829443 180507 :vravn!~vravn@syn.rook.sx QUIT :Excess Flood < 1394829678 577674 :vravn!~vravn@syn.rook.sx JOIN :#esoteric < 1394830222 300396 :nooodl!~nooodl@91.177.69.110 JOIN :#esoteric < 1394830623 848642 :password2_!~password@197.78.152.2 QUIT :Quit: Leaving < 1394830648 836165 :password2!~password@197.78.152.2 QUIT :Remote host closed the connection < 1394830880 77178 :spiette!~spiette@mtl.savoirfairelinux.net QUIT :Quit: :qa! < 1394831170 558409 :vravn!~vravn@syn.rook.sx QUIT :Excess Flood < 1394831298 534080 :vravn!~vravn@syn.rook.sx JOIN :#esoteric < 1394831896 313963 :vravn!~vravn@syn.rook.sx QUIT :Excess Flood < 1394831958 329579 :vravn!~vravn@syn.rook.sx JOIN :#esoteric < 1394833332 844939 :von_cheam!~voncheam@host-92-28-185-26.as13285.net JOIN :#esoteric < 1394833357 843389 :von_cheam!~voncheam@host-92-28-185-26.as13285.net QUIT :Quit: Leaving. < 1394833641 329597 :FireFly!~firefly@oftn/member/FireFly QUIT :Excess Flood < 1394833714 730751 :FireFly!~firefly@oftn/member/FireFly JOIN :#esoteric < 1394833965 687612 :nisstyre!~yourstrul@oftn/member/Nisstyre JOIN :#esoteric < 1394834043 973255 :drlemon!~drlemon@cpe-108-185-0-32.socal.res.rr.com JOIN :#esoteric < 1394834111 19092 :nisstyre_!~yourstrul@oftn/member/Nisstyre JOIN :#esoteric < 1394834254 196005 :nooodl_!~nooodl@91.177.69.110 JOIN :#esoteric < 1394834281 184885 :nooodl!~nooodl@91.177.69.110 QUIT :Ping timeout: 240 seconds < 1394834364 187511 :oerjan!oerjan@sprocket.nvg.ntnu.no JOIN :#esoteric < 1394834452 394976 :shikhout!~Shikhin@unaffiliated/shikhin JOIN :#esoteric < 1394834527 83384 :boily!~boily@96.127.201.149 JOIN :#esoteric < 1394834628 906148 :shikhin!~Shikhin@unaffiliated/shikhin QUIT :Ping timeout: 255 seconds < 1394834630 587253 :shikhout!~Shikhin@unaffiliated/shikhin NICK :shikhin < 1394835063 882903 :luserdroog!636c1b05@gateway/web/freenode/ip.99.108.27.5 QUIT :Ping timeout: 245 seconds < 1394835201 873019 :metasepia!~metasepia@96.127.201.149 JOIN :#esoteric < 1394835248 794628 :von_cheam!~voncheam@host-92-28-185-26.as13285.net JOIN :#esoteric < 1394835258 286415 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :`relcome von_cheam < 1394835277 161678 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :Gregor: the gregorbots, they are dead. < 1394835420 451682 :FireFly!~firefly@oftn/member/FireFly PRIVMSG #esoteric :fungot: staying alive? < 1394835420 627587 :fungot!fis@eos.zem.fi PRIVMSG #esoteric :FireFly: it's the crown, lass, no sense being angry about it now, and he was in the army, too true, and v's still there now and you can. < 1394835428 277520 :FireFly!~firefly@oftn/member/FireFly PRIVMSG #esoteric :dubious. < 1394835470 968364 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :FireFly: you're a lass? < 1394835580 297090 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :alas, no answer < 1394835591 803233 :itsy!~digital_w@87.112.13.30 JOIN :#esoteric < 1394835645 485268 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :gørjand kveld. < 1394835656 423092 :FireFly!~firefly@oftn/member/FireFly PRIVMSG #esoteric :I don't think so < 1394835659 653709 :FireFly!~firefly@oftn/member/FireFly PRIVMSG #esoteric :No last I checked, anyway < 1394835672 315656 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :oerjan: he didn't answer while he was having instant surgery. < 1394835687 116119 :nooodl__!~nooodl@91.177.69.110 JOIN :#esoteric < 1394835696 732612 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :boily: fiendish < 1394835716 11427 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :goedenavnooodln. < 1394835733 938859 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :boilyn soir < 1394835775 705975 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :*boilynsoir < 1394835874 711748 :nooodl_!~nooodl@91.177.69.110 QUIT :Ping timeout: 240 seconds < 1394835983 613804 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :oerjan: today, I read an old blog post showing how to implement monads in Java. it wasn't pretty. < 1394836233 391202 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :boily: Was it http://logicaltypes.blogspot.fi/2011/09/monads-in-java.html ? < 1394836304 634390 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :fizzie: it was. < 1394836316 437306 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :I think that was discussed either here or nearby. < 1394836341 94458 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :are you implying that there are circumesöteric channels? < 1394836387 313543 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :I can only find the "Monads in plain JavaScript" post by gwepping. < 1394836537 582296 :von_cheam!~voncheam@host-92-28-185-26.as13285.net PART :#esoteric < 1394836917 746681 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :pretty sure #haskell is a circumesöteric channel, in any case < 1394837074 860219 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :The evidence for that is circumstantial. < 1394837106 553990 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :that's just circumventing the facts < 1394837406 519471 :olsner!~salparot@c83-252-203-32.bredband.comhem.se PRIVMSG #esoteric :aren't you guys just circumnavigating the topic now? < 1394837592 379459 :olsner!~salparot@c83-252-203-32.bredband.comhem.se PRIVMSG #esoteric :hmm, throws Failure ... is that the Java-monad counterpart of fail? < 1394837962 756525 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :I can't really be bothered to read through it all -- was the Java monad the one where you can't have "Just null", or am I thinking of something else? < 1394838044 265123 :quintopia!~quintopia@unaffiliated/quintopia PRIVMSG #esoteric :helloily < 1394838471 535444 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :quinthellopia! < 1394838552 275946 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :(meanwhile, duck tape with penguins on it? → https://tw-projects.s3.amazonaws.com/twduckbrand/prod/images/products/penguin-duct-tape.jpg) < 1394838587 938846 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :fizzie: I haven't read through it all, but I wouldn't be surprised. Java nulls are very thoroughly pernicious. < 1394838616 604592 :quintopia!~quintopia@unaffiliated/quintopia PRIVMSG #esoteric :there is every kind of duct tape < 1394838637 757523 :quintopia!~quintopia@unaffiliated/quintopia PRIVMSG #esoteric :i went to buy plain old duct tape at walmart once and could only find spongebob, hello kitty, and bacon < 1394838640 962514 :quintopia!~quintopia@unaffiliated/quintopia PRIVMSG #esoteric :i went with bacon < 1394838654 115134 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :nooooo! why didn't you choose the hello kitty one? < 1394838718 711498 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :I like my duck tape gray. same thing with my coffee: black. < 1394838726 681069 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :(and my bagels: poppyseed.) < 1394838733 47219 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net JOIN :#esoteric < 1394838734 681633 :nisstyre_!~yourstrul@oftn/member/Nisstyre QUIT :Quit: WeeChat 0.4.3 < 1394838882 529612 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :> "please don't kill me oerjan" < 1394838883 689665 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : "please don't kill me oerjan" < 1394838884 920156 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :04"please don't kill me oerjan" : 12String < 1394838937 655860 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :ooooooooh... < 1394838948 505922 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :ACTION is all sparkly-anime-eyes < 1394839060 363205 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :~eval "please don't kill me either twh" < 1394839060 420699 :metasepia!~metasepia@96.127.201.149 PRIVMSG #esoteric :Error (127): < 1394839070 414036 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :... < 1394839098 55703 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :@messages-public < 1394839098 168285 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric :Unknown command, try @list < 1394839102 4206 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :@messages-loud < 1394839102 128685 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric :oerjan said 9h 40m 7s ago: please use idris-ircslave's new ( prefix hth < 1394839107 10797 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :( 1 + 1 < 1394839107 123280 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :042 : 12Integer < 1394839115 255631 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :( Integer + Integer < 1394839115 405104 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :Can't resolve type class 12Num 12Type < 1394839134 83572 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :( S -1 < 1394839134 194666 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :Can't resolve type class 12Num (12Nat -> 12Nat) < 1394839140 995192 :yorick!~yorick@oftn/member/yorick JOIN :#esoteric < 1394839142 89297 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :( S (-1) < 1394839142 315488 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :041 : 12Nat < 1394839148 403366 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :uh < 1394839152 265123 :lexande!arapp@terpsichore.ugcs.caltech.edu PRIVMSG #esoteric :o_0 < 1394839167 377379 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :> the Nat (-10) < 1394839167 489550 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :040 : 12Nat < 1394839168 608798 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : Not in scope: `the'Not in scope: data constructor `Nat' < 1394839171 905498 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :oops < 1394839201 321814 :Slereah__!~jackal@176.222.51.233 QUIT :Ping timeout: 240 seconds < 1394839225 602427 :quintopia!~quintopia@unaffiliated/quintopia PRIVMSG #esoteric :boily: i prefer black heavy duty duct tape < 1394839266 309592 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :( the Nat (2-3) < 1394839266 461767 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :040 : 12Nat < 1394839274 720816 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :quintopia: what kind of tape is that? the only two kind of black heavy duty tape I know about are «tape électrique» and that textured one you put on hockey sticks. < 1394839277 349161 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :( the Int (2-3) < 1394839277 496551 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :04-1 : 12Int < 1394839290 185597 :Slereah_!~jackal@176.222.51.233 JOIN :#esoteric < 1394839291 8233 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :( the Int 99999999999999999999999999999999999 < 1394839291 120454 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :043136633892082024447 : 12Int < 1394839292 797127 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :(yes. we call it «tape» in French.) < 1394839306 43913 :quintopia!~quintopia@unaffiliated/quintopia PRIVMSG #esoteric :boily: it's like duct tape, but black rather than silver, and thicker and tougher and harder to tear < 1394839315 518133 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :boily: we call it "teip" in norwegian hth < 1394839333 490873 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Wonder if this could be used to prove 0=1 < 1394839345 770466 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :quintopia: hmm... my curiosity is titillated. < 1394839357 560074 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :oerjan: makes sense. < 1394839362 618849 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Maybe not, once you have a Nat you always have something 0 or greater < 1394839366 970895 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :Sgeo: you realize that this is just how subtraction is defined on Nats, no? < 1394839375 197575 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :What you do before it may be irrelev... o.O < 1394839378 314660 :quintopia!~quintopia@unaffiliated/quintopia PRIVMSG #esoteric :Sgeo: uh...no. in practice, it's illegal to do 2-3 in the naturals < 1394839381 353561 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :I thought Idris was in the wrong < 1394839400 374918 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :> log 3136633892082024447 / log 2 < 1394839400 486856 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :0461.44392285561078 : 12Float < 1394839401 531673 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : 61.44392285561078 < 1394839411 899416 :elliott_!~elliott@unaffiliated/elliott PRIVMSG #esoteric :Sgeo: no because the proof would rely on the definition of - < 1394839431 354816 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :~duck 3136633892082024447 < 1394839431 762849 :metasepia!~metasepia@96.127.201.149 PRIVMSG #esoteric :3136633892082024447 < 1394839503 394687 :quintopia!~quintopia@unaffiliated/quintopia PRIVMSG #esoteric :boily: http://m.shoplet.com/Duck-Heavy-Duty-Duct-Tape/DUCCD3BLACK/ < 1394839549 584462 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :@run 99999999999999999999999999999999999 :: Int64 < 1394839550 798430 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : 3136633892082024447 < 1394839568 608732 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :it's just mod 2^64 < 1394839583 507006 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :I can't write a useful {n : Nat} -> Vect n a -> Nat, can I? < 1394839614 226684 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Or.. something like that, to determine the size of a Vect whose size is unknown at compile-time? < 1394839652 56427 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :( :t Vect < 1394839652 168214 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :12Prelude.Vect.Vect : 12Nat -> 12Type -> 12Type < 1394839676 468007 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :( :t Vect 2 < 1394839676 690200 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :12Vect (09fromInteger 042) : 12Type -> 12Type < 1394839694 861131 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :( :t Vect 2 Bool < 1394839694 972449 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :12Vect (09fromInteger 042) 12Bool : 12Type < 1394839699 160871 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :( Vect 2 Bool < 1394839699 272742 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :12Vect 042 12Bool : 12Type < 1394839723 753618 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :quintopia: the link, it doesn't work. < 1394839737 211854 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :oerjan: meh :/ < 1394839748 54157 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :I assume that doing that (wanting the size that's known only at runtime) is why dependent pairs exist? < 1394839757 310490 :quintopia!~quintopia@unaffiliated/quintopia PRIVMSG #esoteric :boily: i cut a bunch of stuff off the end of it. try cutting more stuff off < 1394839780 21385 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :( the (Vect n a) [1,2,3] < 1394839781 698071 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :(input):1:11:No such variable n < 1394839791 622860 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :( the (Vect _ _) [1,2,3] < 1394839791 770583 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :04[04104, 04204, 04304] : 12Vect 043 12Integer < 1394839811 455590 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :( the Integer 99999999999999999999999999999999999 < 1394839813 398009 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :0499999999999999999999999999999999999 : 12Integer < 1394839824 907614 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :( the (_ ** (Vect _ _)) [1,2,3] < 1394839825 20307 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :Can't unify < 1394839825 131174 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric : 12Vect (04S 13n) 13a < 1394839825 243112 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :with < 1394839825 300146 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric : 04(13x 04** 12Vect 13__pi_arg 13__pi_arg104) < 1394839825 300288 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :Specifically:14↵… < 1394839837 811846 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :( the (_ ** (Vect _ _)) (_ ** [1,2,3]) < 1394839838 34427 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :Can't unify < 1394839838 91370 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric : 12Exists 13a 13P < 1394839838 91510 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :with < 1394839838 91600 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric : 04(13x 04** 12Vect 13__pi_arg 13__pi_arg104) < 1394839838 91694 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :Specifically:14↵… < 1394839852 518578 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :( the (n ** (Vect n _)) (_ ** [1,2,3]) < 1394839852 743313 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :Can't disambiguate name: Data.HVect.::, Prelude.List.::, Data.Vect.Quantifiers.::, Prelude.Stream.::, Prelude.Vect.:: < 1394839873 124715 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :( the (n ** (Vect n _)) (_ ** with Vect [1,2,3]) < 1394839873 384819 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :Can't unify < 1394839873 441048 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric : 12Vect 043 12Integer < 1394839873 441189 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :with < 1394839873 441280 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric : (\13n => 12Vect 13n [__]) 13x < 1394839873 441368 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :Specifically:14↵… < 1394839905 706580 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :quintopia: it still doesn't work. I am saddened :( < 1394839910 482199 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :( the (n ** Vect n String) (_ ** ["1", "2", "3"]) < 1394839910 594200 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :04(043 04** 04[04"1"04, 04"2"04, 04"3"04]04) : 12(13n 12** 12Vect 13n 12String12) < 1394839984 487766 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :huh < 1394840015 484257 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :oerjan: (t ** t)s are useless, right? Or are they not useless somehow < 1394840042 90312 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :how do you find the first element of a ** < 1394840057 565880 :FreeFull!~freefull@defocus/sausage-lover PRIVMSG #esoteric :Sgeo: A value whose type is dependent on itself? < 1394840093 583876 :FreeFull!~freefull@defocus/sausage-lover PRIVMSG #esoteric :> fst (3 ** [1,2,3]) < 1394840093 696278 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :Can't unify < 1394840093 808601 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric : 12Exists 13a 13P < 1394840093 865043 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :with < 1394840093 865229 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric : 12(13iType12, 13t12) < 1394840093 865321 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :Specifically:14↵… < 1394840094 633913 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : Couldn't match expected type `(a0, b0)' with actual type `[t0]' < 1394840107 826437 :FreeFull!~freefull@defocus/sausage-lover PRIVMSG #esoteric :> head (3 ** [1,2,3]) < 1394840108 50468 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :Can't unify < 1394840108 108114 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric : 12Exists 13a 13P < 1394840108 108277 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :with < 1394840108 108369 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric : 12Vect (04S 13n) 13iType < 1394840108 108464 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :Specifically:14↵… < 1394840108 945777 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : No instance for (GHC.Show.Show a0) < 1394840109 168806 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : arising from a use of `M707592794521593570827224.show_M7075927945215935708... < 1394840109 225589 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : The type variable `a0' is ambiguous < 1394840109 225736 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : Possible fix: add a type signature that fixes these type variable(s) < 1394840109 225828 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric : Note: there are several potential instances: < 1394840120 779989 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :( (\v -> let (n ** _) = the (m ** Vect m _) (_ ** v) in n) [1,2,3] < 1394840121 25801 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :(input):1:58:No such variable \ < 1394840121 760651 :FreeFull!~freefull@defocus/sausage-lover PRIVMSG #esoteric :Oh, lambdabot + idris-ircslave < 1394840133 230364 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :oops how do lambdas work < 1394840154 385163 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :( sin < 1394840154 496791 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :09sin : 12Float -> 12Float < 1394840163 49101 :FreeFull!~freefull@defocus/sausage-lover PRIVMSG #esoteric :oerjan: => rather than -> < 1394840166 68454 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net JOIN :#esoteric < 1394840171 441593 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :( (\v => let (n ** _) = the (m ** Vect m _) (_ ** v) in n) [1,2,3] < 1394840174 200149 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :(input):1:58:Can't disambiguate name: Data.HVect.::, Prelude.List.::, Data.Vect.Quantifiers.::, Prelude.Stream.::, Prelude.Vect.:: < 1394840186 110957 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :oops < 1394840200 306109 :FreeFull!~freefull@defocus/sausage-lover PRIVMSG #esoteric :Why ( and not )? < 1394840201 691918 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :( (\(v : Vect _ _) => let (n ** _) = the (m ** Vect m _) (_ ** v) in n) [1,2,3] < 1394840202 65793 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :(input):1:3: error: expected: lambda expression < 1394840202 178263 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :(\(v : Vect _ _) => let (n ** _) = the (m ** Vect m _) (_ ** v) in n) [1,2,3]<> < 1394840202 234250 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric : ^ < 1394840204 917988 :FreeFull!~freefull@defocus/sausage-lover PRIVMSG #esoteric :) 3 < 1394840205 432019 :jconn!~va@1-130.ipswich.cc.colocall.com PRIVMSG #esoteric :FreeFull: 3 < 1394840208 106914 :FreeFull!~freefull@defocus/sausage-lover PRIVMSG #esoteric :A < 1394840219 726399 :FreeFull!~freefull@defocus/sausage-lover PRIVMSG #esoteric :} 3 < 1394840221 864616 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :ok i'm clearly not understanding this < 1394840225 465902 :FreeFull!~freefull@defocus/sausage-lover PRIVMSG #esoteric :} is free < 1394840244 364235 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :^prefixes < 1394840244 476261 :fungot!fis@eos.zem.fi PRIVMSG #esoteric :Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-ircslave ( , jconn ) , blsqbot ! < 1394840255 749113 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :FreeFull: because that is finally now matchin hth < 1394840260 395695 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :*+g < 1394840280 240646 :FreeFull!~freefull@defocus/sausage-lover PRIVMSG #esoteric :( is a weird prefix though < 1394840280 353575 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :No such variable is < 1394840288 806284 :FreeFull!~freefull@defocus/sausage-lover PRIVMSG #esoteric :( exists < 1394840290 349988 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :(input):1:1:No such variable exists < 1394840307 976215 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :ACTION glares angrily at Quassel < 1394840318 983198 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :( Exists < 1394840319 440171 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :12Exists : (13a : 12Type) -> (13a -> 12Type) -> 12Type < 1394840330 77853 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :( Ex_intro < 1394840330 589337 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :(input):0:0:Incomplete term 04Ex_intro < 1394840337 32503 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :( :t Ex_intro < 1394840337 380181 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :04Ex_intro : (13x : 13a) -> (13P 13x) -> 12Exists 13a 13P < 1394840392 136767 :erdic_!erdic@2604:180::6050:fab4 JOIN :#esoteric < 1394840412 987941 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :( let data Foo = Bar | Baz in Foo < 1394840413 664617 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :(input):1:5: error: expected: expression < 1394840413 721983 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :let data Foo = Bar | Baz in Foo < 1394840413 722179 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric : ^ < 1394840419 55759 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :aww < 1394840428 404627 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Isn't there a language that allows local data definitions? < 1394840448 507467 :FreeFull!~freefull@defocus/sausage-lover PRIVMSG #esoteric :Remove the let < 1394840465 485726 :FreeFull!~freefull@defocus/sausage-lover PRIVMSG #esoteric :( data Foo = Bar | Baz < 1394840465 598348 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :(input):1:1: error: expected: ":", < 1394840465 749211 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric : end of input, operator < 1394840465 804842 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :data Foo = Bar | Baz < 1394840465 805004 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net PRIVMSG #esoteric :^ < 1394840476 301987 :FreeFull!~freefull@defocus/sausage-lover PRIVMSG #esoteric :Hmm, maybe not < 1394840674 11945 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net QUIT :*.net *.split < 1394840674 306291 :erdic!erdic@unaffiliated/motley QUIT :*.net *.split < 1394840675 371679 :glogbackup!~glogbacku@192.3.160.190 QUIT :*.net *.split < 1394840675 371816 :Slereahphone!~slereahph@193.253.170.149 QUIT :*.net *.split < 1394840675 371885 :FireFly!~firefly@oftn/member/FireFly QUIT :*.net *.split < 1394840704 886185 :erdic_!erdic@2604:180::6050:fab4 QUIT :Changing host < 1394840704 940961 :erdic_!erdic@unaffiliated/motley JOIN :#esoteric < 1394840991 998220 :mysanthrop!~myname@84.200.43.57 JOIN :#esoteric < 1394841016 993100 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :( the (a ** b) (5 ** "Hi") < 1394841047 204875 :atehwa_!atehwa@aulis.sange.fi JOIN :#esoteric < 1394841050 148545 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :? < 1394841061 680460 :erdic!erdic@2604:180::6050:fab4 JOIN :#esoteric < 1394841090 197325 :tromp_!~tromp@ool-4570a22a.dyn.optonline.net JOIN :#esoteric < 1394841100 511879 :Sgeo_!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :( 1 + 1 < 1394841203 874832 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :Melvar: Sgeo_ killed yer bot hth < 1394841241 992601 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :( "hi" < 1394841264 152901 :fizzie`!fis@unaffiliated/fizzie JOIN :#esoteric < 1394841282 628260 :kmc!~keegan@ec2-50-17-127-187.compute-1.amazonaws.com PRIVMSG #esoteric :just because we don't feel flesh doesn't mean we don't fear death < 1394841354 30150 :erdic_!erdic@unaffiliated/motley QUIT :*.net *.split < 1394841356 812343 :atehwa!atehwa@aulis.sange.fi QUIT :*.net *.split < 1394841356 812476 :Frooxius!~Frooxius@cust-101.ktknet.cz QUIT :*.net *.split < 1394841356 812544 :myname!~myname@84.200.43.57 QUIT :*.net *.split < 1394841356 812613 :idris-ircslave!~ircslave@dslb-088-078-249-067.pools.arcor-ip.net QUIT :*.net *.split < 1394841356 812677 :trout!root@freebsd/developer/variable QUIT :*.net *.split < 1394841356 812741 :pikhq!~pikhq@2602:100:18b2:fbfb:a60:6eff:fece:493 QUIT :*.net *.split < 1394841356 812806 :trn!jhj@2600:3c00::f03c:91ff:feae:3efa QUIT :*.net *.split < 1394841356 812871 :fizzie!fis@unaffiliated/fizzie QUIT :*.net *.split < 1394841385 492586 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :or not. < 1394841488 482888 :fizzie`!fis@unaffiliated/fizzie NICK :fizzie < 1394841510 81270 :pikhq!~pikhq@2602:100:18b2:fbfb:a60:6eff:fece:493 JOIN :#esoteric < 1394841558 48118 :sebbu2!~sebbu@ADijon-152-1-42-203.w83-194.abo.wanadoo.fr JOIN :#esoteric < 1394841590 855942 :sebbu2!~sebbu@ADijon-152-1-42-203.w83-194.abo.wanadoo.fr QUIT :Changing host < 1394841590 911778 :sebbu2!~sebbu@unaffiliated/sebbu JOIN :#esoteric