< 1403136001 573021 :shikhout!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1403136137 340818 :yorick!~yorick@oftn/member/yorick QUIT :Remote host closed the connection < 1403136185 64416 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :gah i run out of moisturizing cream and the itching on my hands immediately drives me crazy < 1403136223 906576 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Ping timeout: 272 seconds < 1403136516 605326 :Froox!~Frooxius@cust-101.ktknet.cz QUIT :Quit: *bubbles away* < 1403136787 891594 :Bike!~Glossina@174-25-61-225.ptld.qwest.net QUIT :Ping timeout: 240 seconds < 1403137643 524583 :Bike!~Glossina@75-175-77-109.ptld.qwest.net JOIN :#esoteric < 1403137912 491345 :Bike!~Glossina@75-175-77-109.ptld.qwest.net QUIT :Ping timeout: 245 seconds < 1403138361 518668 :boily!~boily@96.127.201.149 JOIN :#esoteric < 1403138457 122217 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :back from the dentist. my mouth is now metalless! < 1403138526 2292 :coppro!raedford@taurine.csclub.uwaterloo.ca PRIVMSG #esoteric :congratulations! < 1403138615 98858 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :it feels incredibly weird to suddenly not have a metal wire running behind one's teeth. < 1403138660 886292 :Bike!~Glossina@75-175-77-109.ptld.qwest.net JOIN :#esoteric < 1403139010 396545 :coppro!raedford@taurine.csclub.uwaterloo.ca PRIVMSG #esoteric :yeah < 1403139048 161861 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :and I had a new set of impressions made. next week I'll get a bite splint. < 1403139214 534891 :mhi^!~mhi@unaffiliated/mhi/x-9993184 QUIT :Quit: Lost terminal < 1403139302 735404 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :. o O ( I wonder what's the MRSP of a jug of alginate ) < 1403139482 123785 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :heh. a quick search turns out that a pound of dental alginate runs for about 12 bucks. < 1403139663 851212 :Bike!~Glossina@75-175-77-109.ptld.qwest.net QUIT :Ping timeout: 264 seconds < 1403139741 590028 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :~duck MRSP < 1403139753 882868 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :hmph < 1403139759 63962 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :@google MRSP < 1403139760 457205 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric :http://www.abbreviations.com/MRSP < 1403139760 644425 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric :Title: What does MRSP stand for? < 1403139767 887717 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :VERY USEFUL < 1403139769 358877 :Bike!~Glossina@174-25-46-228.ptld.qwest.net JOIN :#esoteric < 1403139843 843183 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :
ACTION is not sure any of those fit boily's sentence
< 1403139869 600138 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :oh wait that one < 1403140089 569602 :metasepia!~metasepia@96.127.201.149 JOIN :#esoteric < 1403140094 176267 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :~duck MRSP < 1403140094 364105 :metasepia!~metasepia@96.127.201.149 PRIVMSG #esoteric :MrsP.com is a free children's entertainment website. It stars actress Kathy Kinney as Mrs. P, a redheaded Irishwoman who reads classic children's stories from her "Magic Library." The target audience for the website is kids between the ages of 3-12, and its goal is to "encourage a lifetime love of reading." It has no advertising and no subscription fees. The site is produced by Mrs P Enterprises, LLC and was created by Kinney, who played Mimi on The < 1403140099 635340 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :eeeeeeeh... < 1403140109 67335 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :clearly what you meant < 1403140112 995655 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :now in agora: a bug that people exploit by voting, retracting their vote, then revoting in the opposite way. < 1403140144 773372 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :and the exploit being? < 1403140260 838628 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :there's a reward for having voted opposite of the outcome of a proposal < 1403140280 125561 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :and a bug in the phrasing that was _supposed_ to exclude retractions. < 1403140350 639415 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :elegant. < 1403140553 257894 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Maybe I should get back into Agora someday < 1403140590 329344 :Bike!~Glossina@174-25-46-228.ptld.qwest.net QUIT :Ping timeout: 255 seconds < 1403140634 517355 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :oerjan: which proposal? I'm curious < 1403140691 866298 :Bike!~Glossina@174-25-58-12.ptld.qwest.net JOIN :#esoteric < 1403140698 378185 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :And/or was the rule in question present June 3rd? < 1403140745 621784 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :rule 2421/3 < 1403140804 490661 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :don't recall exactly when it was amended < 1403140821 791949 :coppro!raedford@taurine.csclub.uwaterloo.ca PRIVMSG #esoteric :Sgeo: you should < 1403140823 664432 :coppro!raedford@taurine.csclub.uwaterloo.ca PRIVMSG #esoteric :it's happening again < 1403140831 841157 :coppro!raedford@taurine.csclub.uwaterloo.ca PRIVMSG #esoteric :I'm atm writing a really good judgment < 1403140886 906710 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :also, all proposals. < 1403140901 789602 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Oh! < 1403140915 221650 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :It tricked me for a moment into thinking there wasn't a bug < 1403140969 379326 :coppro!raedford@taurine.csclub.uwaterloo.ca PRIVMSG #esoteric :yeah, didn't it :) < 1403140991 927982 :coppro!raedford@taurine.csclub.uwaterloo.ca PRIVMSG #esoteric :nobody noticed until my proposal to reenact the same text < 1403141160 727271 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :For some reason I was thinking I didn't touch Agora since 2008, but I got involved for a bit last year < 1403141282 328420 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :was it during the anniversary celebration? < 1403141377 656097 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Around that time but unrelated to it. Was trying an Ambassador scam < 1403141388 520460 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :ah < 1403141462 529669 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Oh, apparently Agora XX was involved in a counterscam < 1403141814 807190 :boily!~boily@96.127.201.149 QUIT :Quit: PAIRED CHICKEN < 1403141817 121189 :metasepia!~metasepia@96.127.201.149 QUIT :Remote host closed the connection < 1403144883 836706 :Bike!~Glossina@174-25-58-12.ptld.qwest.net QUIT :Ping timeout: 264 seconds < 1403145126 646776 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Erlang/Tcl comparison time: Both Erlang and Tcl have mutable objects be not automatically GCed, while some immutable objects get GCed automatically < 1403145272 657378 :Bike!~Glossina@67-5-229-133.ptld.qwest.net JOIN :#esoteric < 1403145307 937450 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :Wait, you can still go to ancient Greek gathering places? < 1403145366 192700 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :MDude's name is giving me flashbacks to that M person in B < 1403145381 498136 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :MDude: http://agoranomic.org/ < 1403145403 269803 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :People are already asking me if I'm a fat guy's sense of motivation. < 1403145417 179593 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :huh? < 1403145439 435196 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :http://www.whompcomic.com/ < 1403145468 505443 :Bike_!~Glossina@67-5-232-97.ptld.qwest.net JOIN :#esoteric < 1403145489 659260 :pikhq!~pikhq@2602:100:18b2:fbfb:a60:6eff:fece:493 PRIVMSG #esoteric :Sgeo: Strictly speaking, Tcl has *no* GC whatsoever. < 1403145515 560294 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :I thought strings were GCed? < 1403145533 644484 :pikhq!~pikhq@2602:100:18b2:fbfb:a60:6eff:fece:493 PRIVMSG #esoteric :Tcl's semantics are such that there can't be cyclic references, so for simplicity's sake it reference counts instead. < 1403145544 353547 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Ah < 1403145595 557743 :Bike!~Glossina@67-5-229-133.ptld.qwest.net QUIT :Ping timeout: 240 seconds < 1403145601 517210 :Bike_!~Glossina@67-5-232-97.ptld.qwest.net NICK :Bike < 1403146570 719044 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :help im arguing with someone online, i don't want to be the asshole who argues with people online < 1403146649 301395 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :I t hink that you shouldn't do that, and are a bad person for doing it. < 1403146711 285239 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Actually, my reluctance to argue with people who directly contradict me may be hurting me at my job < 1403146808 477898 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :no it isn't! < 1403147146 104113 :^v!~notnot^v@c-71-238-153-166.hsd1.mi.comcast.net QUIT :Read error: Connection reset by peer < 1403147354 763876 :^v!~notnot^v@c-71-238-153-166.hsd1.mi.comcast.net JOIN :#esoteric < 1403148186 546310 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :copumpkin: it was _Liking What You See: A Documentary_ by Ted Chiang < 1403148203 647069 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I'm not sure whether the text is online. < 1403148209 73658 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :http://www.ibooksonline.com/88/Text/liking.html exists but has terrible formatting. < 1403148267 683761 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :it exists but you don't like what you see < 1403148289 75521 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :Sgeo: Are you arguing online with someone you work with at your job? < 1403148310 772908 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Separate arguments, but technically both are online < 1403148311 330479 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :Or do you just need to pracice argue so you're a better arguer at work? < 1403148330 893149 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :The work one's through email, this other one's through Reddit < 1403148339 919979 :copumpkin!~copumpkin@unaffiliated/copumpkin PRIVMSG #esoteric :shachaf: ah, I see < 1403148343 688939 :copumpkin!~copumpkin@unaffiliated/copumpkin PRIVMSG #esoteric :I didn't read it :/ sorry < 1403148350 402345 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :whoa, whoa, whoa < 1403148367 286702 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :no reason to apologize < 1403148400 220980 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :i asked because i thought you were ignoring my questions about it and i didn't want to be bugging you if you weren't interested < 1403148401 289478 :copumpkin!~copumpkin@unaffiliated/copumpkin PRIVMSG #esoteric :well, I said I would :P < 1403148403 799586 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :also this is a different channel < 1403148409 248312 :copumpkin!~copumpkin@unaffiliated/copumpkin PRIVMSG #esoteric :oh, it wasn't intentional ignoring < 1403148413 415350 :copumpkin!~copumpkin@unaffiliated/copumpkin PRIVMSG #esoteric :sorry about that < 1403148414 527857 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :https://docs.google.com/viewer?url=http://glacierpeak.sno.wednet.edu/teachers/bjuhl/docs/Soph%20English/Second%20Semester/Alienation,%20Tolerance,%20Cyrano/Related%20Poems,%20Articles,%20Short%20Stories,%20Etc/Liking%20What%20You%20See%20Portrait%20Version.doc might be slightly better, if more convoluted. < 1403148419 131841 :copumpkin!~copumpkin@unaffiliated/copumpkin PRIVMSG #esoteric :I'm barely at my computer these days < 1403148430 110169 :copumpkin!~copumpkin@unaffiliated/copumpkin PRIVMSG #esoteric :check up on it every so often, get into a chat or two and then go elsewhere < 1403148451 751950 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :i think kmc recommended it too < 1403148456 996964 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :he's not in this channel anymore, though < 1403148470 88963 :copumpkin!~copumpkin@unaffiliated/copumpkin PRIVMSG #esoteric :oh why'd he leave? :( < 1403148546 628198 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :i'm not the person to ask < 1403148663 26688 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :wait is he gone completely < 1403148807 164657 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :oh well he's on freenode somewhere < 1403148994 812395 :copumpkin!~copumpkin@unaffiliated/copumpkin PRIVMSG #esoteric :pity < 1403150192 280800 :oerjan!oerjan@sprocket.nvg.ntnu.no QUIT :Quit: Nite < 1403150272 65753 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :copumpkin: what have you been doing < 1403150284 198521 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :people things < 1403150327 786422 :copumpkin!~copumpkin@unaffiliated/copumpkin PRIVMSG #esoteric :hrm, working a lot, traveling to visit gf (she matched, graduated, went to china, just moved, and I did much of that with her), hanging out with work colleagues, stuff like that < 1403150358 809811 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :matched? < 1403150373 93292 :copumpkin!~copumpkin@unaffiliated/copumpkin PRIVMSG #esoteric :residency match program for med students < 1403150397 319592 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :oh < 1403150397 619928 :copumpkin!~copumpkin@unaffiliated/copumpkin PRIVMSG #esoteric :giant algorithm matching people to hospitals they'll spend the next few years in < 1403150435 922053 :drdanmaku!uid17782@gateway/web/irccloud.com/x-hoiwlyfukfewpabn QUIT :Ping timeout: 272 seconds < 1403150542 936125 :drdanmaku!uid17782@gateway/web/irccloud.com/x-lrodlyxtugjxaywy JOIN :#esoteric < 1403150700 193663 :drdanmaku!uid17782@gateway/web/irccloud.com/x-lrodlyxtugjxaywy QUIT :Client Quit < 1403150808 202459 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :Out of context that sounds like it might be way to decide how to beat people up very bad. < 1403151703 52066 :copumpkin!~copumpkin@unaffiliated/copumpkin PRIVMSG #esoteric ::) < 1403152866 69494 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net NICK :MDream < 1403152938 658624 :Sorella!~queen@oftn/member/Sorella QUIT :Quit: It is tiem! < 1403153610 831676 :variable!root@freebsd/developer/variable NICK :function < 1403154955 920094 :shikhout!~shikhin@unaffiliated/shikhin QUIT :Ping timeout: 240 seconds < 1403155961 664344 :Aetherspawn-!uid6924@gateway/web/irccloud.com/x-osxfpqrozvxljdid JOIN :#esoteric < 1403156278 117069 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :So, in a theorem prover thingie, what exactly is a "tactic"? I swear i've heard about such things. < 1403156443 200303 :newsham!~chat@udp217044uds.hawaiiantel.net PRIVMSG #esoteric :a proof search algorithm < 1403156558 680590 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :Could you elaborate. < 1403156711 888755 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :what kind of elaboration < 1403156727 261877 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :something a silly person like me could perhaps begin to understand. < 1403156806 976091 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :a program that tries to write a proof term for a certain subset of propositions < 1403156819 47047 :newsham!~chat@udp217044uds.hawaiiantel.net PRIVMSG #esoteric :http://www.cis.upenn.edu/~bcpierce/sf/current/toc.html provides a reasonable introduction < 1403156823 173697 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :usually in some ugly turing-complete language, no real hard guarantees < 1403157016 927078 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :thanks < 1403157084 269779 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :i wonder if i should just try going through this damn thing, i have enough books already < 1403157105 759552 :newsham!~chat@udp217044uds.hawaiiantel.net PRIVMSG #esoteric :you start of with a statement of what you want a functions type to be, and you have some other functions which can do parts of the solution for that function, giving you a simpler type (goal) to work towards < 1403157119 133652 :newsham!~chat@udp217044uds.hawaiiantel.net PRIVMSG #esoteric :its like an interactive program solver.. you nudge it along and it does a lot of the grunt work < 1403157134 809731 :newsham!~chat@udp217044uds.hawaiiantel.net PRIVMSG #esoteric :you wont have to go very far in SF before you learn what a tactic is < 1403157144 101622 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :SF? < 1403157151 116781 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :oh, this book. < 1403157152 308267 :newsham!~chat@udp217044uds.hawaiiantel.net PRIVMSG #esoteric :the sf/current/toc.html book < 1403157174 905548 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :well, i kind of don't want to read about booleans for the billionth time. especially since i'm probably never going to use coq. you know? < 1403157197 669622 :FreeFull!~freefull@defocus/sausage-lover QUIT : < 1403157318 501434 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :booleans? < 1403157325 879231 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :coq doesn't really involve all that many of those < 1403157335 73079 :newsham!~chat@udp217044uds.hawaiiantel.net PRIVMSG #esoteric :sf starts out with a few boolean examples < 1403157340 446176 :newsham!~chat@udp217044uds.hawaiiantel.net PRIVMSG #esoteric :dont worry, it goes quickly from there < 1403157346 996376 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :Bike: you may like chlipala's CPDT < 1403157352 775344 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :just glancing at the table of contents, with enumerated data types < 1403157358 117704 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :it has nicer proof style than SF < 1403157361 216253 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :http://adam.chlipala.net/cpdt/ < 1403157378 362219 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :it's the coq manual :p < 1403157395 157049 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :(heavy tactics focus) < 1403157408 125145 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :Can I just ask things here? < 1403157423 982007 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :sure, if you want. I'm too tired to answer questions though. < 1403157443 595048 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :@localtime elliott < 1403157444 928428 :lambdabot!~lambdabot@silicon.int-e.eu PRIVMSG #esoteric :Local time for elliott is Thu Jun 19 06:57:23 2014 < 1403157457 11141 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :well it's super basic. like, you said tactics are in some ugly imperative language, so presumably they're outside of the coq system, not written in coq? < 1403157477 699490 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :they're in a metalanguage as part of the coq system < 1403157484 573446 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :though they can also be written in ocaml, like the built-in ones are < 1403157714 8286 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :hm this "coq reference manual" which may or may not be what you just linked might be what i want < 1403157819 217408 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :sf has this as an example: "Theorem plus_O_n : ∀n : nat, 0 + n = n. Proof. intros n. reflexivity. Qed." the intros n and reflexivity are steps to do the proof? like we start with the 0 + n thing, intros n fires, that gets you something else (probably n = n), then reflexivity fires and reduces it to true? < 1403157870 810365 :newsham!~chat@udp217044uds.hawaiiantel.net PRIVMSG #esoteric :yah, "intros" and "reflexitivity" are tactics. < 1403157908 583459 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :Bike: I was joking when I called CPDT the Coq manual. < 1403157913 380617 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :it's more like the Coq manual they forgot to write. < 1403157915 520116 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :oh. < 1403157918 787944 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :well, i am also tired. < 1403157951 226473 :newsham!~chat@udp217044uds.hawaiiantel.net PRIVMSG #esoteric :you should try to load the SF example in proof general, and step through the proof.. for each stepp it will show you what is known in the environment and what the goal is < 1403157959 431185 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :hm. < 1403157960 185858 :newsham!~chat@udp217044uds.hawaiiantel.net PRIVMSG #esoteric :and the tactics "intros" and "reflexivity" will update those < 1403157967 783551 :newsham!~chat@udp217044uds.hawaiiantel.net PRIVMSG #esoteric :you can single step through the proof that way interactively < 1403157989 723032 :newsham!~chat@udp217044uds.hawaiiantel.net PRIVMSG #esoteric :its a shame there is no "live coq" web site that lets you do this online < 1403157991 855587 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :well, why not (besides that i haven't installed an emacs mode in so long) < 1403158047 229966 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :blugh my distro doesn't have coq in the main repos < 1403158057 917605 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :really? < 1403158059 64115 :newsham!~chat@udp217044uds.hawaiiantel.net PRIVMSG #esoteric :you can prob find a livecd to boot in a virtual machine < 1403158139 565248 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :elliott: yeah, it's in the AUR. not hard to install or anything, but a bit annoying < 1403158147 684199 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :and it comes with some IDE for some reason? whatever, less work maybe < 1403158221 289033 :newsham!~chat@udp217044uds.hawaiiantel.net PRIVMSG #esoteric :oh, it looks like there are some SF youtube vids < 1403158231 777332 :newsham!~chat@udp217044uds.hawaiiantel.net PRIVMSG #esoteric :maybe they would have good walktrhoughs of some proofs < 1403158277 689206 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :i'm looking at this for weird reasons nobody here would probably like < 1403158344 701156 :newsham!~chat@udp217044uds.hawaiiantel.net PRIVMSG #esoteric :the great thing about knowledge, we dont have to approve < 1403158520 570786 :Bike!~Glossina@67-5-232-97.ptld.qwest.net PRIVMSG #esoteric :you say that now, but watch me use coq to sink california < 1403158873 380497 :newsham!~chat@udp217044uds.hawaiiantel.net PRIVMSG #esoteric :you're working for a hedge fund? < 1403161327 170185 :FireFly!~firefly@oftn/member/FireFly QUIT :Excess Flood < 1403161390 408731 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :`coins < 1403161390 408886 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :^coins < 1403161429 697618 :Effilry!~firefly@firefly.xen.prgmr.com JOIN :#esoteric < 1403161603 979656 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :I'm hoping for something like: 3100,182,4,10001coin 10866,3582,22002,22002coin 192,1051,25,1056coin 11652,22252,23004,22002coin 8500,,4, 3001,,,coin < 1403161610 897310 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :no < 1403161617 832483 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :3100,182,4,10001coin 10866,3582,22002,22002coin 192,1051,25,1056coin 11652,22252,23004,22002coin 8500,,4,coin 3001,,,coin > 1403162630 767022 JOIN :#esoteric > 1403162634 890080 JOIN :#esoteric > 1403162635 404848 JOIN :#esoteric > 1403162686 344710 JOIN :#esoteric > 1403162690 467706 JOIN :#esoteric > 1403162690 982598 JOIN :#esoteric > 1403162717 427832 JOIN :#esoteric > 1403162721 550915 JOIN :#esoteric > 1403162722 66253 JOIN :#esoteric > 1403162748 528667 JOIN :#esoteric > 1403162752 648500 JOIN :#esoteric > 1403162753 164029 JOIN :#esoteric > 1403162810 345410 JOIN :#esoteric > 1403162814 468480 JOIN :#esoteric > 1403162814 984068 JOIN :#esoteric > 1403162841 411499 JOIN :#esoteric > 1403162845 533541 JOIN :#esoteric > 1403162846 48304 JOIN :#esoteric > 1403162872 434704 JOIN :#esoteric > 1403162876 556498 JOIN :#esoteric > 1403162877 71958 JOIN :#esoteric > 1403162905 940384 JOIN :#esoteric < 1403162907 34870 :glogbot!dlopen@libdl.so JOIN :#esoteric < 1403162907 88401 :card.freenode.net NOTICE #esoteric :[freenode-info] please register your nickname...don't forget to auto-identify! http://freenode.net/faq.shtml#nicksetup > 1403162910 64648 JOIN :#esoteric > 1403162910 579779 JOIN :#esoteric < 1403162945 810624 :realzies!~pinky@unaffiliated/realazthat JOIN :#esoteric < 1403163038 689303 :slereah_!~slereah@46.218.232.202 JOIN :#esoteric < 1403165092 114097 :password2!~password@197.78.206.224 JOIN :#esoteric < 1403165375 126715 :Tritonio!~Thunderbi@212.251.54.186 JOIN :#esoteric < 1403165625 263217 :password2!~password@197.78.206.224 QUIT :Ping timeout: 244 seconds < 1403165704 479512 :contrapumpkin!~copumpkin@unaffiliated/copumpkin JOIN :#esoteric < 1403165939 978088 :copumpkin!~copumpkin@unaffiliated/copumpkin QUIT :Ping timeout: 272 seconds < 1403166446 488470 :password2!~password@197.78.206.224 JOIN :#esoteric < 1403166681 402076 :Patashu!~Patashu@c27-253-115-204.carlnfd2.nsw.optusnet.com.au JOIN :#esoteric < 1403167081 276921 :Patashu_!Helix@c27-253-115-204.carlnfd2.nsw.optusnet.com.au JOIN :#esoteric < 1403167081 571142 :Patashu!~Patashu@c27-253-115-204.carlnfd2.nsw.optusnet.com.au QUIT :Disconnected by services < 1403167149 601554 :MindlessDrone!~MindlessD@unaffiliated/mindlessdrone JOIN :#esoteric < 1403167553 24100 :Patashu!~Patashu@c27-253-115-204.carlnfd2.nsw.optusnet.com.au JOIN :#esoteric < 1403167656 411172 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover JOIN :#esoteric < 1403167764 270512 :Patashu_!Helix@c27-253-115-204.carlnfd2.nsw.optusnet.com.au QUIT :Ping timeout: 244 seconds < 1403168662 564944 :password2!~password@197.78.206.224 QUIT :Ping timeout: 245 seconds < 1403169242 980470 :nooodl!~nooodl@77.104-242-81.adsl-dyn.isp.belgacom.be JOIN :#esoteric < 1403170401 624166 :nooodl!~nooodl@77.104-242-81.adsl-dyn.isp.belgacom.be QUIT :Quit: Ik ga weg < 1403171398 367856 :conehead!~conehead@unaffiliated/conehead QUIT :Quit: Computer has gone to sleep < 1403172256 870923 :barrucad1!~barrucadu@fsf/member/barrucadu NICK :barrucadu < 1403172940 599879 :boily!~boily@96.127.201.149 JOIN :#esoteric < 1403174286 603752 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover QUIT :Ping timeout: 255 seconds < 1403174308 596027 :MoALTz!~no@user-46-112-93-173.play-internet.pl JOIN :#esoteric < 1403175683 958251 :boily!~boily@96.127.201.149 QUIT :Quit: PLASMA CHICKEN < 1403177261 451193 :Effilry!~firefly@firefly.xen.prgmr.com PRIVMSG #esoteric :BANCcoin? < 1403177332 439579 :Effilry!~firefly@firefly.xen.prgmr.com QUIT :Changing host < 1403177332 494345 :Effilry!~firefly@oftn/member/FireFly JOIN :#esoteric < 1403177341 478085 :Effilry!~firefly@oftn/member/FireFly NICK :FireFly < 1403177547 327805 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :Hmm. < 1403177665 953046 :HackEgo!~HackEgo@162.248.166.242 JOIN :#esoteric < 1403177670 669502 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :There we: go. < 1403177671 955683 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :`coins < 1403177673 248393 :HackEgo!~HackEgo@162.248.166.242 PRIVMSG #esoteric :​08bizobcoin 09pbocoin 02qweverpacoin 06rutcrtlcoin 13vowelcoin 04jumcoin 07kethaxcoin 08twositcoin 09fitcoin 02auticonformcoin 06jash-01coin 13haniacoin 04tediumbraincoin 07hunkatorecoin 08omecoin 09thestaicoin 02chocoin 06velacoin 13palcoin 04revoycoin < 1403177702 953949 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :fungot: Couldn't you take care of your fellow bots? < 1403177703 830413 :fungot!fis@eos.zem.fi PRIVMSG #esoteric :fizzie: so the way it does and it reports a problem on 1 exercise... 1 exercise i really dont have a clue understand his point ( because the fnord one that chances are if you never exit? that book sucks. < 1403177782 861249 :Melvar!~melvar@dslb-092-072-175-242.pools.arcor-ip.net PRIVMSG #esoteric :( the (3 `LTE` 5) (tactics search) < 1403177784 28909 :idris-bot!~ircslave@dslb-092-072-175-242.pools.arcor-ip.net PRIVMSG #esoteric :04lteSucc (04lteSucc (04lteSucc 04lteZero)) : 12LTE 043 045 < 1403177842 530999 :Melvar!~melvar@dslb-092-072-175-242.pools.arcor-ip.net PRIVMSG #esoteric :Bike: ↑ The search tactic in Idris mostly just tries constructors, which works for simple things like this. < 1403179111 852131 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :fizzie: thanks < 1403179121 817320 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :`coins < 1403179123 52281 :HackEgo!~HackEgo@162.248.166.242 PRIVMSG #esoteric :​04timensifticcoin 07andcoin 08rubicoin 09eodcoin 02poikecoin 06wailcoin 13morascoin 04contcoin 07dobeycoin 08quotecoin 09spiuntinecoin 02mismcoin 06monecoin 13existcoin 04agrtecoin 07boarceacoin 08braincoin 09illgaudeliumcoin 02factcoin 06tapascoin < 1403179128 255643 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :^style BANCStar < 1403179128 344425 :fungot!fis@eos.zem.fi PRIVMSG #esoteric :Not found. < 1403179265 344967 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net QUIT :Read error: Connection reset by peer < 1403180338 223058 :oerjan!oerjan@sprocket.nvg.ntnu.no JOIN :#esoteric < 1403180542 127187 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :overheared coworker in meeting room saying "it's all the same because it's Turing complete" < 1403180693 544345 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :b_jonas: just start giving him code in befunge hth < 1403180698 590255 :polytone_!~monotone@room208.org NICK :monotone < 1403180712 644992 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :*funge-98 < 1403181124 416548 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :is funge-98 the one with bounded memory? < 1403181133 781448 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :or only bounded code space? < 1403181137 333112 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :let me check the wiki < 1403181309 679626 :yorick!~yorick@oftn/member/yorick JOIN :#esoteric < 1403181328 372818 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :right, funge-98 allows arbitrary playfield dimensions, < 1403181586 596640 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :I wonder if my old olvashato language counts as esoteric < 1403181606 62506 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :it wasn't designed to be difficult to program in, so it might not count < 1403181684 818550 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :let me look up the official definition < 1403181705 777746 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :"An esoteric programming language is a computer programming language designed to experiment with weird ideas, to be hard to program in, or as a joke, rather than for practical use." -- I could argue either way < 1403181984 590457 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :http://catseye.tc/node/The_Aesthetics_of_Esolangs is my preferred vague definition of esoteric, I think < 1403181984 752451 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :how can a language whose name means "readable" be esoteric that's absurd < 1403182218 931114 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :also why won't ó work on google's pages in my browser < 1403182256 600976 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :or ´ accents at all < 1403182312 939557 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :b_jonas: i corrected to funge-98 to make it clear i meant the tc variant. < 1403182332 616339 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :or well, less un-tc. not sure if there are still some limits. < 1403182361 287649 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :funge-98 is at least as-TC-as-C, I think < 1403182363 531879 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :oerjan: too late to rename < 1403182369 437669 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :OKAY < 1403182370 98995 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :and has enough holes that there's probably something TC hiding in there < 1403182376 803418 :elliott!~elliott@unaffiliated/elliott PRIVMSG #esoteric :especially with fingerprints < 1403182509 687989 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :oerjan: the original purpose was to make a language in which I write ugly source code, and it's compiled to readable standard ml and readable prolog code; but I sort of ran out of time and the readable part got dropped so now the compiled code is even more ugly than the original < 1403182548 59091 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :I might be able to make the output a bit more readable if I fix the indenting (though that's not trivial) and throw in some peep-hole beautification rules < 1403182570 482049 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :(it already has some of the latter, but needs more) < 1403182576 261137 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :`addquote oerjan: the original purpose was to make a language in which I write ugly source code, and it's compiled to readable standard ml and readable prolog code; but I sort of ran out of time and < 1403182577 728565 :HackEgo!~HackEgo@162.248.166.242 PRIVMSG #esoteric :1207) oerjan: the original purpose was to make a language in which I write ugly source code, and it's compiled to readable standard ml and readable prolog code; but I sort of ran out of time and < 1403182580 333425 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric : the readable part got dropped so now the compiled code is even < 1403182582 920607 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric : more ugly than the original < 1403182589 975113 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :`revert < 1403182595 432292 :HackEgo!~HackEgo@162.248.166.242 PRIVMSG #esoteric :Done. < 1403182600 635585 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :bloody irssi line merging worked half-way < 1403182632 281644 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :`addquote oerjan: the original purpose was to make a language in which I write ugly source code, and it's compiled to readable standard ml and readable prolog code; but I sort of ran out of time and the readable part got dropped so now the compiled code is even more ugly than the original < 1403182633 747698 :HackEgo!~HackEgo@162.248.166.242 PRIVMSG #esoteric :1207) oerjan: the original purpose was to make a language in which I write ugly source code, and it's compiled to readable standard ml and readable prolog code; but I sort of ran out of time and the readable part got dropped so now the compiled code is even more ugly than the original < 1403182662 643340 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :stuff's already here, for ages: http://www.math.bme.hu/~ambrus/pu/olvashato/ < 1403182666 705657 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :but with not much docs < 1403182839 477687 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :i am pretty sure using ruby to compile something into prolog and sml is blasphemic hth < 1403182857 986295 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :why? < 1403182906 790240 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :because sml is the language that's supposed to be good for implementing compilers in < 1403182948 412128 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :what? I thought sml is supposed to be a general-purpose language with definition available only in some expensive book < 1403182990 257094 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :well it is general purpose, but ml was _created_ for implementing other languages in < 1403183000 155596 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :the name stands for "meta-language" < 1403183009 786808 :slereah_!~slereah@46.218.232.202 PRIVMSG #esoteric :Gaiz how do I computer < 1403183049 413040 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :of course ocaml and haskell are also good examples, being similar in the ways that matter. < 1403183051 912755 :slereah_!~slereah@46.218.232.202 PRIVMSG #esoteric :I am trying to write over some text of console, but so far nothing works D: < 1403183067 308429 :slereah_!~slereah@46.218.232.202 PRIVMSG #esoteric :Neither fflush nor printf("\b") nor ncurses < 1403183095 750607 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :hm how much has sml been hurt in recent years by being closed-documentation < 1403183110 465096 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :
ACTION is just wondering
< 1403183143 320949 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :slereah_: try printf("\b\x7f") to overpunch the character with delete so the column is skipped when the tape is read back < 1403183153 460148 :slereah_!~slereah@46.218.232.202 PRIVMSG #esoteric :I shall try < 1403183171 542878 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :i suspect prolog is also good to write implementations in. erlang was originally written in it? < 1403183201 920551 :slereah_!~slereah@46.218.232.202 PRIVMSG #esoteric :Nope, it just writes \x7f as the unicode character 007f < 1403183242 989765 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :oerjan: I did consider writing an interpreter in prolog and one in sml plus only a minimal translator that translates the syntax of the program to a data structure in the input syntax of those two languages < 1403183246 471284 :Patashu!~Patashu@c27-253-115-204.carlnfd2.nsw.optusnet.com.au QUIT :Ping timeout: 240 seconds < 1403183273 363552 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :(such as pushes parenthesis and throws in some commas) < 1403183282 853815 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :but I decide it wouldn't be simpler < 1403183312 777138 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :and I'd likely lose points the result because it's interpreted crap < 1403183341 120483 :slereah_!~slereah@46.218.232.202 PRIVMSG #esoteric :Ah, I think I see < 1403183352 24496 :slereah_!~slereah@46.218.232.202 PRIVMSG #esoteric :You need to use \r instead of \n in hthe text < 1403183405 302869 :slereah_!~slereah@46.218.232.202 PRIVMSG #esoteric :Except now only one line displays instead of the three < 1403183409 934725 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :b_jonas: hm it looks lispy < 1403183410 347494 :slereah_!~slereah@46.218.232.202 PRIVMSG #esoteric :How bothersome < 1403183438 834169 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :oerjan: yes, in particular it's like scheme in that the head of function calls are evaluated the same as other parts < 1403183446 421353 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :no wait < 1403183448 753111 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :are they? < 1403183450 439012 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :let me check < 1403183477 586728 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :quite the opposite < 1403183492 955283 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :it's common lispy in that the head of function calls is evaluated differently than the arguments < 1403183500 316749 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :lisp-2, check < 1403183520 422924 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :that's why there's a primitive function |call| just like in clisp < 1403183546 615957 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :but the |let| builtin has a syntax different from lisps < 1403183661 694042 :b_jonas!~x@russell2.math.bme.hu PRIVMSG #esoteric :it's implementable as a lisp macro, but has an unnatural syntax < 1403183691 869736 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :and here i though b_jonas was your real name < 1403184191 395773 :FreeFull!~freefull@defocus/sausage-lover JOIN :#esoteric < 1403185713 369764 :lollo64it!~lorenzo@93-58-3-33.ip156.fastwebnet.it QUIT :Ping timeout: 244 seconds < 1403185976 113411 :password2!~password@197.78.206.129 JOIN :#esoteric < 1403187365 894546 :Sorella!~queen@oftn/member/Sorella JOIN :#esoteric < 1403188078 990922 :edwardk!~edwardk@pdpc/supporter/professional/edwardk JOIN :#esoteric < 1403188634 996430 :edwardk!~edwardk@pdpc/supporter/professional/edwardk QUIT :Quit: Computer has gone to sleep. < 1403188722 532423 :brandonson!~brandonso@d173-180-174-224.bchsia.telus.net QUIT :Read error: Connection reset by peer < 1403188758 609263 :brandonson!~brandonso@d173-180-174-224.bchsia.telus.net JOIN :#esoteric < 1403188786 709212 :brandonson!~brandonso@d173-180-174-224.bchsia.telus.net QUIT :Read error: Connection reset by peer < 1403188806 260812 :brandonson!~brandonso@d173-180-174-224.bchsia.telus.net JOIN :#esoteric < 1403188930 845739 :edwardk!~edwardk@pdpc/supporter/professional/edwardk JOIN :#esoteric < 1403190475 981361 :mihow!~mihow@rrcs-50-75-208-18.nyc.biz.rr.com JOIN :#esoteric < 1403190871 317164 :Aetherspawn-!uid6924@gateway/web/irccloud.com/x-osxfpqrozvxljdid QUIT :Quit: Connection closed for inactivity < 1403192047 444461 :edwardk!~edwardk@pdpc/supporter/professional/edwardk QUIT :Quit: Computer has gone to sleep. < 1403192523 517559 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover JOIN :#esoteric < 1403192803 37725 :olsner_!~salparot@c83-252-201-82.bredband.comhem.se PRIVMSG #esoteric :elliott: I don't remember going, I remember coming back < 1403192906 740007 :Tritonio!~Thunderbi@212.251.54.186 QUIT :Ping timeout: 240 seconds < 1403193204 379260 :edwardk!~edwardk@pdpc/supporter/professional/edwardk JOIN :#esoteric < 1403193497 829847 :olsner_!~salparot@c83-252-201-82.bredband.comhem.se NICK :olsner < 1403193677 62872 :slereah_!~slereah@46.218.232.202 QUIT :Quit: Leaving < 1403193773 527151 :edwardk!~edwardk@pdpc/supporter/professional/edwardk QUIT :Ping timeout: 244 seconds < 1403194319 185840 :oerjan!oerjan@sprocket.nvg.ntnu.no QUIT :Quit: Yay money < 1403194570 469706 :edwardk!~edwardk@pdpc/supporter/professional/edwardk JOIN :#esoteric < 1403194858 990068 :drdanmaku!uid17782@gateway/web/irccloud.com/x-zoncjovtrywmodxq JOIN :#esoteric < 1403196867 476658 :Tritonio!~Thunderbi@athedsl-21632.home.otenet.gr JOIN :#esoteric < 1403196964 247931 :^v!~notnot^v@c-71-238-153-166.hsd1.mi.comcast.net NICK :gabensale2014 < 1403198266 160337 :mihow!~mihow@rrcs-50-75-208-18.nyc.biz.rr.com QUIT :Quit: mihow < 1403199564 973865 :gabensale2014!~notnot^v@c-71-238-153-166.hsd1.mi.comcast.net NICK :^0 < 1403199605 326358 :lollo64it!~lorenzo@93-58-3-33.ip156.fastwebnet.it JOIN :#esoteric < 1403199835 966979 :MDream!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net QUIT :Ping timeout: 272 seconds < 1403201339 831123 :Tritonio!~Thunderbi@athedsl-21632.home.otenet.gr QUIT :*.net *.split < 1403201341 546317 :edwardk!~edwardk@pdpc/supporter/professional/edwardk QUIT :*.net *.split < 1403201342 657181 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover QUIT :*.net *.split < 1403201346 457255 :FreeFull!~freefull@defocus/sausage-lover QUIT :*.net *.split < 1403201349 708513 :contrapumpkin!~copumpkin@unaffiliated/copumpkin QUIT :*.net *.split < 1403201357 604110 :impomatic!~digital_w@84.93.80.151 QUIT :*.net *.split < 1403201359 387670 :heroux!~heroux@50708181.static.ziggozakelijk.nl QUIT :*.net *.split < 1403201384 282592 :barrucadu!~barrucadu@fsf/member/barrucadu QUIT :*.net *.split < 1403201393 604417 :hogeyui_!~hogeyuiVP@vps.usamimi.biz QUIT :*.net *.split < 1403201395 676799 :lifthrasiir!~lifthrasi@115.68.131.49 QUIT :*.net *.split < 1403201404 223497 :idris-bot!~ircslave@dslb-092-072-175-242.pools.arcor-ip.net QUIT :*.net *.split < 1403201433 846024 :realzies!~pinky@unaffiliated/realazthat QUIT :*.net *.split < 1403201434 512217 :Gregor!dlopen@libdl.so QUIT :*.net *.split < 1403201435 603994 :monotone!~monotone@room208.org QUIT :*.net *.split < 1403201439 685317 :augur!~augur@216-164-48-148.c3-0.slvr-ubr1.lnh-slvr.md.cable.rcn.com QUIT :*.net *.split < 1403201448 691343 :aloril!~aloril@dsl-tkubrasgw2-54f80b-12.dhcp.inet.fi QUIT :*.net *.split < 1403201449 300734 :Slereah!~jackal@176.222.51.233 QUIT :*.net *.split < 1403201451 200220 :HackEgo!~HackEgo@162.248.166.242 QUIT :*.net *.split < 1403201458 743711 :KingOfKarlsruhe!~KingOfKar@unaffiliated/kingofkarlsruhe QUIT :*.net *.split < 1403201469 248139 :drdanmaku!uid17782@gateway/web/irccloud.com/x-zoncjovtrywmodxq QUIT :*.net *.split < 1403201505 633175 :b_jonas!~x@russell2.math.bme.hu QUIT :*.net *.split < 1403201508 129358 :shachaf!~shachaf@unaffiliated/shachaf QUIT :*.net *.split < 1403201514 529126 :tromp__!~tromp@rtc35-154.rentec.com QUIT :*.net *.split < 1403201534 503680 :MoALTz!~no@user-46-112-93-173.play-internet.pl QUIT :*.net *.split < 1403201535 523949 :MindlessDrone!~MindlessD@unaffiliated/mindlessdrone QUIT :*.net *.split < 1403201539 964882 :Bike!~Glossina@67-5-232-97.ptld.qwest.net QUIT :*.net *.split < 1403201540 636686 :sebbu!~sebbu@unaffiliated/sebbu QUIT :*.net *.split < 1403201541 81527 :Sprocklem!~sprocklem@unaffiliated/sprocklem QUIT :*.net *.split < 1403201544 860972 :constant!root@freebsd/developer/variable QUIT :*.net *.split < 1403201546 331754 :TodPunk!Tod@50-198-177-186-static.hfc.comcastbusiness.net QUIT :*.net *.split < 1403201552 748694 :Melvar!~melvar@dslb-092-072-175-242.pools.arcor-ip.net QUIT :*.net *.split < 1403201567 777485 :nortti!nortti@nano.smar.fi QUIT :*.net *.split < 1403201585 925289 :kyhwana!kyhwana@snowleopard.kyhwana.org QUIT :*.net *.split < 1403201589 386051 :Burton!Burton@gateway/shell/bouncerstation/x-kabfjjybaleettsh QUIT :*.net *.split < 1403201595 754035 :Taneb!~Taneb@runciman.hacksoc.org QUIT :*.net *.split < 1403201605 868896 :ski!~ski@remote1.student.chalmers.se QUIT :*.net *.split < 1403201630 570196 :douglass!~iridium@home-on-the-dome.mit.edu QUIT :*.net *.split < 1403201634 261108 :jix_!~jix@jixco.de QUIT :*.net *.split < 1403201639 507933 :diginet!~diginet@107.170.146.29 QUIT :*.net *.split < 1403201652 243343 :ineiros!~itniemin@bayesianconspiracy.org QUIT :*.net *.split < 1403201654 915222 :maurer!~maurer@MIMUNG.ECE.CMU.EDU QUIT :*.net *.split < 1403201656 226419 :elliott!~elliott@unaffiliated/elliott QUIT :*.net *.split < 1403201656 407715 :int-e!~noone@static.88-198-179-137.clients.your-server.de QUIT :*.net *.split < 1403201658 951860 :^0!~notnot^v@c-71-238-153-166.hsd1.mi.comcast.net QUIT :*.net *.split > 1403201666 744528 JOIN :#esoteric > 1403201670 854461 JOIN :#esoteric > 1403201671 370373 JOIN :#esoteric > 1403201713 575747 JOIN :#esoteric < 1403201714 243917 :glogbot!dlopen@libdl.so JOIN :#esoteric > 1403201717 700850 JOIN :#esoteric > 1403201718 215156 JOIN :#esoteric < 1403201785 902282 :mihow!~mihow@rrcs-50-75-208-18.nyc.biz.rr.com JOIN :#esoteric < 1403201786 53136 :lollo64it!~lorenzo@93-58-3-33.ip156.fastwebnet.it JOIN :#esoteric < 1403201786 53270 :brandonson!~brandonso@d173-180-174-224.bchsia.telus.net JOIN :#esoteric < 1403201786 53335 :Sorella!~queen@oftn/member/Sorella JOIN :#esoteric < 1403201786 53398 :17SAAFGOG!dlopen@libdl.so JOIN :#esoteric < 1403201786 53462 :atehwa!atehwa@aulis.sange.fi JOIN :#esoteric < 1403201786 53524 :FireFly!~firefly@oftn/member/FireFly JOIN :#esoteric < 1403201786 53585 :tromp!~tromp@ool-4570a006.dyn.optonline.net JOIN :#esoteric < 1403201786 53646 :coppro!raedford@taurine.csclub.uwaterloo.ca JOIN :#esoteric < 1403201786 53708 :jj2baile!~jon@corn-syrup.csclub.uwaterloo.ca JOIN :#esoteric < 1403201786 53771 :myname!~myname@84.200.43.57 JOIN :#esoteric < 1403201786 53832 :erdic!erdic@unaffiliated/motley JOIN :#esoteric < 1403201786 53893 :`^_^v!~nycs@ip-216-46-79-198.dsl.nyc.megapath.net JOIN :#esoteric < 1403201786 54009 :vravn!~vravn@syn.rook.sx JOIN :#esoteric < 1403201786 54072 :Gracenotes!~person@192.241.203.42 JOIN :#esoteric < 1403201786 54134 :_46bit!sid10106@pdpc/supporter/student/mmokrysz JOIN :#esoteric < 1403201786 54195 :vyv!~vyv@70.51.217.166 JOIN :#esoteric < 1403201786 54256 :mtve!~mtve@10130.x.rootbsd.net JOIN :#esoteric < 1403201786 54319 :clog!~nef@bespin.org JOIN :#esoteric < 1403201786 54379 :pikhq!~pikhq@2602:100:18b2:fbfb:a60:6eff:fece:493 JOIN :#esoteric < 1403201786 54439 :Speed`!~Speed@evile.thrash.im JOIN :#esoteric < 1403201786 54553 :ggherdov!sid11402@gateway/web/irccloud.com/x-uccykrdyqknfxinm JOIN :#esoteric < 1403201786 54615 :newsham!~chat@udp217044uds.hawaiiantel.net JOIN :#esoteric < 1403201853 537504 :atehwa!atehwa@aulis.sange.fi QUIT :Write error: Broken pipe < 1403201853 887285 :17SAAFGOG!dlopen@libdl.so QUIT :Write error: Broken pipe < 1403201854 156821 :jj2baile!~jon@corn-syrup.csclub.uwaterloo.ca QUIT :Write error: Broken pipe < 1403202771 533948 :FireFly!~firefly@oftn/member/FireFly QUIT :Excess Flood < 1403202788 108129 :`^_^v!~nycs@ip-216-46-79-198.dsl.nyc.megapath.net QUIT :Excess Flood < 1403202793 399623 :brandonson!~brandonso@d173-180-174-224.bchsia.telus.net QUIT :Excess Flood < 1403202812 266624 :`^_^v!~nycs@ip-216-46-79-198.dsl.nyc.megapath.net JOIN :#esoteric < 1403202839 319971 :brandonson!~brandonso@173.180.174.224 JOIN :#esoteric < 1403202877 334794 :FireFly!~firefly@oftn/member/FireFly JOIN :#esoteric < 1403204672 502131 :shikhin!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1403205179 518619 :^v!~notnot^v@2601:4:4500:887:bdf7:1f45:19d:6f0b JOIN :#esoteric < 1403205233 735038 :^v!~notnot^v@2601:4:4500:887:bdf7:1f45:19d:6f0b QUIT :Client Quit < 1403206261 779779 :conehead!~conehead@unaffiliated/conehead JOIN :#esoteric < 1403206362 456294 :Bike!~Glossina@67-5-232-97.ptld.qwest.net QUIT :Ping timeout: 245 seconds < 1403206482 505250 :Bike!~Glossina@75-175-78-103.ptld.qwest.net JOIN :#esoteric < 1403206755 733261 :MindlessDrone!~MindlessD@unaffiliated/mindlessdrone QUIT :Quit: MindlessDrone < 1403206801 113648 :olsner!~salparot@c83-252-201-82.bredband.comhem.se PRIVMSG #esoteric :`quote midsummer < 1403206801 645466 :HackEgo!~HackEgo@162.248.166.242 PRIVMSG #esoteric :No output. < 1403206907 577301 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :`quote night's < 1403206908 115700 :HackEgo!~HackEgo@162.248.166.242 PRIVMSG #esoteric :No output. < 1403206913 998876 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :`quote dream < 1403206914 550541 :HackEgo!~HackEgo@162.248.166.242 PRIVMSG #esoteric :147) catseye: Please wake up. Not recorded for this timezone. The big spider is not your dream \ 230) back to legal tender, that expression really makes me daydream. Like, there'd be black-market tender. Out-of-town hug shops where people exchange tenderness you've NEVER SEEN BEFORE. \ 240) Gregor, yeah, but P < 1403206919 280207 :olsner!~salparot@c83-252-201-82.bredband.comhem.se PRIVMSG #esoteric :`quote fixed pattern < 1403206919 809556 :HackEgo!~HackEgo@162.248.166.242 PRIVMSG #esoteric :358) as always in sweden everything goes to a fixed pattern: thursday is queueing at systembolaget to get beer and schnaps, friday is pickled herring, schnaps and dancing the frog dance around the phallos, saturday is dedicated to being hung over < 1403206966 137656 :int-e!~noone@static.88-198-179-137.clients.your-server.de PRIVMSG #esoteric :`quote 240 < 1403206966 654948 :HackEgo!~HackEgo@162.248.166.242 PRIVMSG #esoteric :240) Gregor, yeah, but Purdue has poultry science facilities beyond the dreams of avarice. < 1403207056 916752 :olsner!~salparot@c83-252-201-82.bredband.comhem.se PRIVMSG #esoteric :but I did the systembolaget yesterday, 5 minutes before closing when it was empty, so I neatly evaded the queueing < 1403207282 345782 :olsner!~salparot@c83-252-201-82.bredband.comhem.se PRIVMSG #esoteric :btw, someone just pointed out that the frog dance is likely a jab at the french, imported from english derogative use of "frog" (but frog doesn't really mean that in swedish) < 1403207293 799111 :olsner!~salparot@c83-252-201-82.bredband.comhem.se PRIVMSG #esoteric :it's also danced to a french march < 1403207583 943100 :lifthrasiir!~lifthrasi@115.68.131.49 QUIT :Ping timeout: 240 seconds < 1403207864 560361 :mhi^!~mhi@unaffiliated/mhi/x-9993184 JOIN :#esoteric < 1403207940 778923 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :I like the name "systembolaget". < 1403208152 119511 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :Can't find the etymology in the (English) 'pedia. < 1403208171 526514 :Bike!~Glossina@75-175-78-103.ptld.qwest.net QUIT :Ping timeout: 264 seconds < 1403208194 562286 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :Our counterpart is just called "Alko", which is very boring. < 1403208260 881665 :Bike!~Glossina@75-175-111-165.ptld.qwest.net JOIN :#esoteric < 1403208270 522183 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :The Norwegian version has a refreshingly direct name. ("Vinmonopolet".) < 1403208327 967649 :olsner!~salparot@c83-252-201-82.bredband.comhem.se PRIVMSG #esoteric :yeah, exactly what it says, it's pretty nice < 1403208413 160708 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :"During the 1939-40 Winter War the company [Alko, or Oy Alkoholiliike Ab as it was then called] mass-produced molotov cocktails for the Finnish military, production totalling 450,000 units" heh < 1403208456 102414 :olsner!~salparot@c83-252-201-82.bredband.comhem.se PRIVMSG #esoteric :it seems that "system" comes from http://en.wikipedia.org/wiki/Gothenburg_Public_House_System < 1403208471 702061 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :I see. < 1403208632 508398 :lifthrasiir!~lifthrasi@115.68.131.49 JOIN :#esoteric < 1403208667 777339 :MDream!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net JOIN :#esoteric < 1403208667 927603 :MDream!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net NICK :MDude < 1403209516 550016 :Taneb!~Taneb@runciman.hacksoc.org PRIVMSG #esoteric :applybot: help < 1403209516 703513 :applybot!~applybot@unaffiliated/jafet PRIVMSG #esoteric : Meta-commands: colour context help info load* restart shutdown* state timeout* undo unicode unload* \ Isabelle commands: apply by declare defer definition done find_theorems fun function lemma oops prefer primrec quickcheck term termination thm try0 typ unfolding using value < 1403209830 502334 :Frooxius!~Frooxius@cust-101.ktknet.cz JOIN :#esoteric < 1403210877 53665 :Frooxius!~Frooxius@cust-101.ktknet.cz QUIT :Read error: Connection reset by peer < 1403210932 394673 :Frooxius!~Frooxius@cust-101.ktknet.cz JOIN :#esoteric < 1403211676 777883 :Patashu!~Patashu@c27-253-115-204.carlnfd2.nsw.optusnet.com.au JOIN :#esoteric < 1403212113 143797 :oerjan!oerjan@sprocket.nvg.ntnu.no JOIN :#esoteric < 1403212392 561818 :nortti!nortti@nano.smar.fi NICK :lawspeaker < 1403212412 570894 :lawspeaker!nortti@nano.smar.fi NICK :nortti < 1403212417 601530 :mroman!~roman2@fmnssun.ibone.ch PRIVMSG #esoteric :applybot: state < 1403212418 143289 :applybot!~applybot@unaffiliated/jafet PRIVMSG #esoteric : Not in a proof. < 1403212434 907597 :fizzie!fis@unaffiliated/fizzie PRIVMSG #esoteric :fungot: Prove something. < 1403212435 105248 :fungot!fis@eos.zem.fi PRIVMSG #esoteric :fizzie: src/ ip.h or is it < 1403212455 732802 :mroman!~roman2@fmnssun.ibone.ch PRIVMSG #esoteric :fungot: ls -lah src < 1403212456 32814 :fungot!fis@eos.zem.fi PRIVMSG #esoteric :mroman: damn. he got that. but still patch of green where medialab extension is supposed to < 1403212813 327807 :Patashu!~Patashu@c27-253-115-204.carlnfd2.nsw.optusnet.com.au QUIT :Disconnected by services < 1403212813 478877 :Patashu_!~Patashu@c27-253-115-204.carlnfd2.nsw.optusnet.com.au JOIN :#esoteric < 1403212993 469583 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :applybot: country < 1403212993 657695 :applybot!~applybot@unaffiliated/jafet PRIVMSG #esoteric : *** Unrecognized command < 1403213220 300344 :Patashu_!~Patashu@c27-253-115-204.carlnfd2.nsw.optusnet.com.au QUIT :Ping timeout: 255 seconds < 1403213323 83921 :Sprocklem!~sprocklem@unaffiliated/sprocklem QUIT :Quit: leaving < 1403213340 472788 :Sprocklem!~sprocklem@unaffiliated/sprocklem JOIN :#esoteric < 1403214112 608470 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :applybot: info < 1403214112 758791 :applybot!~applybot@unaffiliated/jafet PRIVMSG #esoteric : Loaded theories: Main "~~/src/HOL/Library/Code_Target_Nat" "~~/src/HOL/Number_Theory/Primes" \ 0 lines in session. \ Command timeout is 20 s. \ Unicode translation disabled. \ Colour output disabled. < 1403214146 780129 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :applybot: help state < 1403214146 930646 :applybot!~applybot@unaffiliated/jafet PRIVMSG #esoteric : state: Show the state of the current proof (if there is one). < 1403214190 505980 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :applyvot: context < 1403214202 320819 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :applybot: help context < 1403214202 480910 :applybot!~applybot@unaffiliated/jafet PRIVMSG #esoteric : context [N]: Show the most recent (N) lines in this session. < 1403214222 223949 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :applybot context 10 < 1403214234 883734 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :applybot: context 10 < 1403214235 34517 :applybot!~applybot@unaffiliated/jafet PRIVMSG #esoteric : Beginning of theory. < 1403214261 109969 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :applybot: help term < 1403214261 260332 :applybot!~applybot@unaffiliated/jafet PRIVMSG #esoteric : term: Isabelle command < 1403214276 389869 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :applybot: help Isabelle < 1403214276 608709 :applybot!~applybot@unaffiliated/jafet PRIVMSG #esoteric : Unknown command: Isabelle < 1403214289 718284 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :applybot: fungot < 1403214289 903965 :applybot!~applybot@unaffiliated/jafet PRIVMSG #esoteric : *** Unrecognized command < 1403214290 54095 :fungot!fis@eos.zem.fi PRIVMSG #esoteric :MDude: in the matter... things will fnord down after this week hopefully. < 1403214603 349496 :boily!~boily@96.127.201.149 JOIN :#esoteric < 1403214658 475883 :metasepia!~metasepia@96.127.201.149 JOIN :#esoteric < 1403214709 206233 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :~duck MSRP < 1403214709 489915 :metasepia!~metasepia@96.127.201.149 PRIVMSG #esoteric :--- No relevant information < 1403214751 881920 :edwardk!~edwardk@pdpc/supporter/professional/edwardk QUIT :Quit: Computer has gone to sleep. < 1403215345 516320 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :`? b_jonas < 1403215346 83615 :HackEgo!~HackEgo@162.248.166.242 PRIVMSG #esoteric :b_jonas? ¯\(°​_o)/¯ < 1403215366 108864 :boily!~boily@96.127.201.149 PRIVMSG #esoteric :an sudden opportunity appears! b_jonas, how would you wisdomically describe yourself? < 1403215449 708358 :HackEgo!~HackEgo@162.248.166.242 PRIVMSG #esoteric :[wiki] 14[[07AlphaBeta14]]4 10 02http://esolangs.org/w/index.php?diff=39860&oldid=34593 5* 03188.192.76.116 5* (+257) 10Added Lua implementation from Michael Armbruster < 1403215825 551844 :nooodl!~nooodl@77.104-242-81.adsl-dyn.isp.belgacom.be JOIN :#esoteric < 1403216925 459626 :boily!~boily@96.127.201.149 QUIT :Quit: INDIAN CHICKEN < 1403216927 862070 :metasepia!~metasepia@96.127.201.149 QUIT :Remote host closed the connection < 1403217567 301681 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover QUIT :Ping timeout: 255 seconds < 1403217759 447371 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover JOIN :#esoteric < 1403218526 736538 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net JOIN :#esoteric < 1403219371 73007 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :~duck help < 1403219389 901669 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :~duck metasepia < 1403219413 302956 :^v!~notnot^v@2601:4:4500:887:6907:95b3:c8c4:65b6 JOIN :#esoteric < 1403219415 37096 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :Oh, metasepia has left. < 1403219495 799222 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :`? metasepia < 1403219496 466606 :HackEgo!~HackEgo@162.248.166.242 PRIVMSG #esoteric :metasepia knows the weather at your nearest airport, and also something about ducks. < 1403219608 975938 :Taneb!~Taneb@runciman.hacksoc.org PRIVMSG #esoteric :`? MDude < 1403219609 620963 :HackEgo!~HackEgo@162.248.166.242 PRIVMSG #esoteric :MDude? ¯\(°​_o)/¯ < 1403219632 416855 :Taneb!~Taneb@runciman.hacksoc.org PRIVMSG #esoteric :`learn MDude is just a dude, with an M's courage. < 1403219634 7620 :HackEgo!~HackEgo@162.248.166.242 PRIVMSG #esoteric :I knew that. < 1403219867 950422 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :are you sure he's not a million dudes < 1403220004 233168 :^v!~notnot^v@2601:4:4500:887:6907:95b3:c8c4:65b6 QUIT :Quit: http://i.imgur.com/Akc6r.gif < 1403220093 694915 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :That would be pretty cool. < 1403220142 829119 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Who was that person in B who blatantly had no idea about anything in the rules? < 1403220177 912564 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :I don't know what B is, so if I was in it I clearly had no idea. < 1403220210 350333 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :`? B < 1403220211 4503 :HackEgo!~HackEgo@162.248.166.242 PRIVMSG #esoteric :B? ¯\(°​_o)/¯ < 1403220221 698215 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :I think that serves as proof that MDude was that person in B < 1403220274 342886 :MDude!~fyrc@or-67-238-17-218.dhcp.embarqhsd.net PRIVMSG #esoteric :It's pretty strong evidence. < 1403220282 736134 :^v!~notnot^v@c-71-238-153-166.hsd1.mi.comcast.net JOIN :#esoteric < 1403220548 388649 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :M P Darke < 1403220807 453856 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover QUIT :Ping timeout: 264 seconds < 1403221046 368486 :shikhout!~shikhin@unaffiliated/shikhin JOIN :#esoteric < 1403221212 467870 :shikhin!~shikhin@unaffiliated/shikhin QUIT :Ping timeout: 245 seconds < 1403221514 158087 :mihow!~mihow@rrcs-50-75-208-18.nyc.biz.rr.com QUIT :Quit: mihow < 1403222140 999878 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :argh i now have _four_ tabs with shtetl-optimized comment threads open that i haven't managed to finish... < 1403222198 295671 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :(even once. i sometimes go back to old ones to check for new comments.) < 1403222250 982350 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :Is that F# monad tutorial that doesn't say 'monad' about monads in general or just the Error monad? < 1403222283 663612 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :it's really a thinly disguised burrito cookbook hth < 1403222358 487133 :Sgeo!~quassel@ool-44c2df0c.dyn.optonline.net PRIVMSG #esoteric :http://www.calcentral.com/~monadrailway/Monad/Welcome.html