00:00:01 -!- shikhout has joined. 00:02:17 -!- yorick has quit (Remote host closed the connection). 00:03:05 gah i run out of moisturizing cream and the itching on my hands immediately drives me crazy 00:03:43 -!- shikhin has quit (Ping timeout: 272 seconds). 00:08:36 -!- Froox has quit (Quit: *bubbles away*). 00:13:07 -!- Bike has quit (Ping timeout: 240 seconds). 00:27:23 -!- Bike has joined. 00:31:52 -!- Bike has quit (Ping timeout: 245 seconds). 00:39:21 -!- boily has joined. 00:40:57 back from the dentist. my mouth is now metalless! 00:42:06 congratulations! 00:43:35 it feels incredibly weird to suddenly not have a metal wire running behind one's teeth. 00:44:20 -!- Bike has joined. 00:50:10 yeah 00:50:48 and I had a new set of impressions made. next week I'll get a bite splint. 00:53:34 -!- mhi^ has quit (Quit: Lost terminal). 00:55:02 . o O ( I wonder what's the MRSP of a jug of alginate ) 00:58:02 heh. a quick search turns out that a pound of dental alginate runs for about 12 bucks. 01:01:03 -!- Bike has quit (Ping timeout: 264 seconds). 01:02:21 ~duck MRSP 01:02:33 hmph 01:02:39 @google MRSP 01:02:40 http://www.abbreviations.com/MRSP 01:02:40 Title: What does MRSP stand for? 01:02:47 VERY USEFUL 01:02:49 -!- Bike has joined. 01:04:03 * oerjan is not sure any of those fit boily's sentence 01:04:29 oh wait that one 01:08:09 -!- metasepia has joined. 01:08:14 ~duck MRSP 01:08:14 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 01:08:19 eeeeeeeh... 01:08:29 clearly what you meant 01:08:32 now in agora: a bug that people exploit by voting, retracting their vote, then revoting in the opposite way. 01:09:04 and the exploit being? 01:11:00 there's a reward for having voted opposite of the outcome of a proposal 01:11:20 and a bug in the phrasing that was _supposed_ to exclude retractions. 01:12:30 elegant. 01:15:53 Maybe I should get back into Agora someday 01:16:30 -!- Bike has quit (Ping timeout: 255 seconds). 01:17:14 oerjan: which proposal? I'm curious 01:18:11 -!- Bike has joined. 01:18:18 And/or was the rule in question present June 3rd? 01:19:05 rule 2421/3 01:20:04 don't recall exactly when it was amended 01:20:21 Sgeo: you should 01:20:23 it's happening again 01:20:31 I'm atm writing a really good judgment 01:21:26 also, all proposals. 01:21:41 Oh! 01:21:55 It tricked me for a moment into thinking there wasn't a bug 01:22:49 yeah, didn't it :) 01:23:11 nobody noticed until my proposal to reenact the same text 01:26:00 For some reason I was thinking I didn't touch Agora since 2008, but I got involved for a bit last year 01:28:02 was it during the anniversary celebration? 01:29:37 Around that time but unrelated to it. Was trying an Ambassador scam 01:29:48 ah 01:31:02 Oh, apparently Agora XX was involved in a counterscam 01:36:54 -!- boily has quit (Quit: PAIRED CHICKEN). 01:36:57 -!- metasepia has quit (Remote host closed the connection). 02:28:03 -!- Bike has quit (Ping timeout: 264 seconds). 02:32:06 Erlang/Tcl comparison time: Both Erlang and Tcl have mutable objects be not automatically GCed, while some immutable objects get GCed automatically 02:34:32 -!- Bike has joined. 02:35:07 Wait, you can still go to ancient Greek gathering places? 02:36:06 MDude's name is giving me flashbacks to that M person in B 02:36:21 MDude: http://agoranomic.org/ 02:36:43 People are already asking me if I'm a fat guy's sense of motivation. 02:36:57 huh? 02:37:19 http://www.whompcomic.com/ 02:37:48 -!- Bike_ has joined. 02:38:09 Sgeo: Strictly speaking, Tcl has *no* GC whatsoever. 02:38:35 I thought strings were GCed? 02:38:53 Tcl's semantics are such that there can't be cyclic references, so for simplicity's sake it reference counts instead. 02:39:04 Ah 02:39:55 -!- Bike has quit (Ping timeout: 240 seconds). 02:40:01 -!- Bike_ has changed nick to Bike. 02:56:10 help im arguing with someone online, i don't want to be the asshole who argues with people online 02:57:29 I t hink that you shouldn't do that, and are a bad person for doing it. 02:58:31 Actually, my reluctance to argue with people who directly contradict me may be hurting me at my job 03:00:08 no it isn't! 03:05:46 -!- ^v has quit (Read error: Connection reset by peer). 03:09:14 -!- ^v has joined. 03:23:06 copumpkin: it was _Liking What You See: A Documentary_ by Ted Chiang 03:23:23 I'm not sure whether the text is online. 03:23:29 http://www.ibooksonline.com/88/Text/liking.html exists but has terrible formatting. 03:24:27 it exists but you don't like what you see 03:24:49 Sgeo: Are you arguing online with someone you work with at your job? 03:25:10 Separate arguments, but technically both are online 03:25:11 Or do you just need to pracice argue so you're a better arguer at work? 03:25:30 The work one's through email, this other one's through Reddit 03:25:39 shachaf: ah, I see 03:25:43 I didn't read it :/ sorry 03:25:50 whoa, whoa, whoa 03:26:07 no reason to apologize 03:26:40 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 03:26:41 well, I said I would :P 03:26:43 also this is a different channel 03:26:49 oh, it wasn't intentional ignoring 03:26:53 sorry about that 03:26:54 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. 03:26:59 I'm barely at my computer these days 03:27:10 check up on it every so often, get into a chat or two and then go elsewhere 03:27:31 i think kmc recommended it too 03:27:36 he's not in this channel anymore, though 03:27:50 oh why'd he leave? :( 03:29:06 i'm not the person to ask 03:31:03 wait is he gone completely 03:33:27 oh well he's on freenode somewhere 03:36:34 pity 03:56:32 -!- oerjan has quit (Quit: Nite). 03:57:52 copumpkin: what have you been doing 03:58:04 people things 03:58:47 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 03:59:18 matched? 03:59:33 residency match program for med students 03:59:57 oh 03:59:57 giant algorithm matching people to hospitals they'll spend the next few years in 04:00:35 -!- drdanmaku has quit (Ping timeout: 272 seconds). 04:02:22 -!- drdanmaku has joined. 04:05:00 -!- drdanmaku has quit (Client Quit). 04:06:48 Out of context that sounds like it might be way to decide how to beat people up very bad. 04:21:43 :) 04:41:06 -!- MDude has changed nick to MDream. 04:42:18 -!- Sorella has quit (Quit: It is tiem!). 04:53:30 -!- variable has changed nick to function. 05:15:55 -!- shikhout has quit (Ping timeout: 240 seconds). 05:32:41 -!- Aetherspawn- has joined. 05:37:58 So, in a theorem prover thingie, what exactly is a "tactic"? I swear i've heard about such things. 05:40:43 a proof search algorithm 05:42:38 Could you elaborate. 05:45:11 what kind of elaboration 05:45:27 something a silly person like me could perhaps begin to understand. 05:46:46 a program that tries to write a proof term for a certain subset of propositions 05:46:59 http://www.cis.upenn.edu/~bcpierce/sf/current/toc.html provides a reasonable introduction 05:47:03 usually in some ugly turing-complete language, no real hard guarantees 05:50:16 thanks 05:51:24 i wonder if i should just try going through this damn thing, i have enough books already 05:51:45 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 05:51:59 its like an interactive program solver.. you nudge it along and it does a lot of the grunt work 05:52:14 you wont have to go very far in SF before you learn what a tactic is 05:52:24 SF? 05:52:31 oh, this book. 05:52:32 the sf/current/toc.html book 05:52:54 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? 05:53:17 -!- FreeFull has quit. 05:55:18 booleans? 05:55:25 coq doesn't really involve all that many of those 05:55:35 sf starts out with a few boolean examples 05:55:40 dont worry, it goes quickly from there 05:55:46 Bike: you may like chlipala's CPDT 05:55:52 just glancing at the table of contents, with enumerated data types 05:55:58 it has nicer proof style than SF 05:56:01 http://adam.chlipala.net/cpdt/ 05:56:18 it's the coq manual :p 05:56:35 (heavy tactics focus) 05:56:48 Can I just ask things here? 05:57:03 sure, if you want. I'm too tired to answer questions though. 05:57:23 @localtime elliott 05:57:24 Local time for elliott is Thu Jun 19 06:57:23 2014 05:57:37 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? 05:57:57 they're in a metalanguage as part of the coq system 05:58:04 though they can also be written in ocaml, like the built-in ones are 06:01:54 hm this "coq reference manual" which may or may not be what you just linked might be what i want 06:03:39 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? 06:04:30 yah, "intros" and "reflexitivity" are tactics. 06:05:08 Bike: I was joking when I called CPDT the Coq manual. 06:05:13 it's more like the Coq manual they forgot to write. 06:05:15 oh. 06:05:18 well, i am also tired. 06:05:51 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 06:05:59 hm. 06:06:00 and the tactics "intros" and "reflexivity" will update those 06:06:07 you can single step through the proof that way interactively 06:06:29 its a shame there is no "live coq" web site that lets you do this online 06:06:31 well, why not (besides that i haven't installed an emacs mode in so long) 06:07:27 blugh my distro doesn't have coq in the main repos 06:07:37 really? 06:07:39 you can prob find a livecd to boot in a virtual machine 06:08:59 elliott: yeah, it's in the AUR. not hard to install or anything, but a bit annoying 06:09:07 and it comes with some IDE for some reason? whatever, less work maybe 06:10:21 oh, it looks like there are some SF youtube vids 06:10:31 maybe they would have good walktrhoughs of some proofs 06:11:17 i'm looking at this for weird reasons nobody here would probably like 06:12:24 the great thing about knowledge, we dont have to approve 06:15:20 you say that now, but watch me use coq to sink california 06:21:13 you're working for a hedge fund? 07:02:07 -!- FireFly has quit (Excess Flood). 07:03:10 `coins 07:03:10 ^coins 07:03:49 -!- Effilry has joined. 07:06:43 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 07:06:50 no 07:06:57 3100,182,4,10001coin 10866,3582,22002,22002coin 192,1051,25,1056coin 11652,22252,23004,22002coin 8500,,4,coin 3001,,,coin 07:23:50 -!- esowiki has joined. 07:23:54 -!- esowiki has joined. 07:23:55 -!- esowiki has joined. 07:24:46 -!- esowiki has joined. 07:24:50 -!- esowiki has joined. 07:24:50 -!- esowiki has joined. 07:25:17 -!- esowiki has joined. 07:25:21 -!- esowiki has joined. 07:25:22 -!- esowiki has joined. 07:25:48 -!- esowiki has joined. 07:25:52 -!- esowiki has joined. 07:25:53 -!- esowiki has joined. 07:26:50 -!- esowiki has joined. 07:26:54 -!- esowiki has joined. 07:26:54 -!- esowiki has joined. 07:27:21 -!- esowiki has joined. 07:27:25 -!- esowiki has joined. 07:27:26 -!- esowiki has joined. 07:27:52 -!- esowiki has joined. 07:27:56 -!- esowiki has joined. 07:27:57 -!- esowiki has joined. 07:28:25 -!- esowiki has joined. 07:28:27 -!- glogbot has joined. 07:28:27 [freenode-info] please register your nickname...don't forget to auto-identify! http://freenode.net/faq.shtml#nicksetup 07:28:30 -!- esowiki has joined. 07:28:30 -!- esowiki has joined. 07:29:05 -!- realzies has joined. 07:30:38 -!- slereah_ has joined. 08:04:52 -!- password2 has joined. 08:09:35 -!- Tritonio has joined. 08:13:45 -!- password2 has quit (Ping timeout: 244 seconds). 08:15:04 -!- contrapumpkin has joined. 08:18:59 -!- copumpkin has quit (Ping timeout: 272 seconds). 08:27:26 -!- password2 has joined. 08:31:21 -!- Patashu has joined. 08:38:01 -!- Patashu_ has joined. 08:38:01 -!- Patashu has quit (Disconnected by services). 08:39:09 -!- MindlessDrone has joined. 08:45:53 -!- Patashu has joined. 08:47:36 -!- Phantom_Hoover has joined. 08:49:24 -!- Patashu_ has quit (Ping timeout: 244 seconds). 09:04:22 -!- password2 has quit (Ping timeout: 245 seconds). 09:14:02 -!- nooodl has joined. 09:33:21 -!- nooodl has quit (Quit: Ik ga weg). 09:49:58 -!- conehead has quit (Quit: Computer has gone to sleep). 10:04:16 -!- barrucad1 has changed nick to barrucadu. 10:15:40 -!- boily has joined. 10:38:06 -!- Phantom_Hoover has quit (Ping timeout: 255 seconds). 10:38:28 -!- MoALTz has joined. 11:01:23 -!- boily has quit (Quit: PLASMA CHICKEN). 11:27:41 BANCcoin? 11:28:52 -!- Effilry has quit (Changing host). 11:28:52 -!- Effilry has joined. 11:29:01 -!- Effilry has changed nick to FireFly. 11:32:27 Hmm. 11:34:25 -!- HackEgo has joined. 11:34:30 There we: go. 11:34:31 `coins 11:34:33 ​bizobcoin pbocoin qweverpacoin rutcrtlcoin vowelcoin jumcoin kethaxcoin twositcoin fitcoin auticonformcoin jash-01coin haniacoin tediumbraincoin hunkatorecoin omecoin thestaicoin chocoin velacoin palcoin revoycoin 11:35:02 fungot: Couldn't you take care of your fellow bots? 11:35:03 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. 11:36:22 ( the (3 `LTE` 5) (tactics search) 11:36:24 lteSucc (lteSucc (lteSucc lteZero)) : LTE 3 5 11:37:22 Bike: ↑ The search tactic in Idris mostly just tries constructors, which works for simple things like this. 11:58:31 fizzie: thanks 11:58:41 `coins 11:58:43 ​timensifticcoin andcoin rubicoin eodcoin poikecoin wailcoin morascoin contcoin dobeycoin quotecoin spiuntinecoin mismcoin monecoin existcoin agrtecoin boarceacoin braincoin illgaudeliumcoin factcoin tapascoin 11:58:48 ^style BANCStar 11:58:48 Not found. 12:01:05 -!- Sgeo has quit (Read error: Connection reset by peer). 12:18:58 -!- oerjan has joined. 12:22:22 overheared coworker in meeting room saying "it's all the same because it's Turing complete" 12:24:53 b_jonas: just start giving him code in befunge hth 12:24:58 -!- polytone_ has changed nick to monotone. 12:25:12 *funge-98 12:32:04 is funge-98 the one with bounded memory? 12:32:13 or only bounded code space? 12:32:17 let me check the wiki 12:35:09 -!- yorick has joined. 12:35:28 right, funge-98 allows arbitrary playfield dimensions, 12:39:46 I wonder if my old olvashato language counts as esoteric 12:40:06 it wasn't designed to be difficult to program in, so it might not count 12:41:24 let me look up the official definition 12:41:45 "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 12:46:24 http://catseye.tc/node/The_Aesthetics_of_Esolangs is my preferred vague definition of esoteric, I think 12:46:24 how can a language whose name means "readable" be esoteric that's absurd 12:50:18 also why won't ó work on google's pages in my browser 12:50:56 or ´ accents at all 12:51:52 b_jonas: i corrected to funge-98 to make it clear i meant the tc variant. 12:52:12 or well, less un-tc. not sure if there are still some limits. 12:52:41 funge-98 is at least as-TC-as-C, I think 12:52:43 oerjan: too late to rename 12:52:49 OKAY 12:52:50 and has enough holes that there's probably something TC hiding in there 12:52:56 especially with fingerprints 12:55:09 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 12:55:48 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 12:56:10 (it already has some of the latter, but needs more) 12:56:16 `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 12:56:17 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 12:56:20 the readable part got dropped so now the compiled code is even 12:56:22 more ugly than the original 12:56:29 `revert 12:56:35 Done. 12:56:40 bloody irssi line merging worked half-way 12:57:12 `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 12:57:13 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 12:57:42 stuff's already here, for ages: http://www.math.bme.hu/~ambrus/pu/olvashato/ 12:57:46 but with not much docs 13:00:39 i am pretty sure using ruby to compile something into prolog and sml is blasphemic hth 13:00:57 why? 13:01:46 because sml is the language that's supposed to be good for implementing compilers in 13:02:28 what? I thought sml is supposed to be a general-purpose language with definition available only in some expensive book 13:03:10 well it is general purpose, but ml was _created_ for implementing other languages in 13:03:20 the name stands for "meta-language" 13:03:29 Gaiz how do I computer 13:04:09 of course ocaml and haskell are also good examples, being similar in the ways that matter. 13:04:11 I am trying to write over some text of console, but so far nothing works D: 13:04:27 Neither fflush nor printf("\b") nor ncurses 13:04:55 hm how much has sml been hurt in recent years by being closed-documentation 13:05:10 * oerjan is just wondering 13:05:43 slereah_: try printf("\b\x7f") to overpunch the character with delete so the column is skipped when the tape is read back 13:05:53 I shall try 13:06:11 i suspect prolog is also good to write implementations in. erlang was originally written in it? 13:06:41 Nope, it just writes \x7f as the unicode character 007f 13:07:22 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 13:07:26 -!- Patashu has quit (Ping timeout: 240 seconds). 13:07:53 (such as pushes parenthesis and throws in some commas) 13:08:02 but I decide it wouldn't be simpler 13:08:32 and I'd likely lose points the result because it's interpreted crap 13:09:01 Ah, I think I see 13:09:12 You need to use \r instead of \n in hthe text 13:10:05 Except now only one line displays instead of the three 13:10:09 b_jonas: hm it looks lispy 13:10:10 How bothersome 13:10:38 oerjan: yes, in particular it's like scheme in that the head of function calls are evaluated the same as other parts 13:10:46 no wait 13:10:48 are they? 13:10:50 let me check 13:11:17 quite the opposite 13:11:32 it's common lispy in that the head of function calls is evaluated differently than the arguments 13:11:40 lisp-2, check 13:12:00 that's why there's a primitive function |call| just like in clisp 13:12:26 but the |let| builtin has a syntax different from lisps 13:14:21 it's implementable as a lisp macro, but has an unnatural syntax 13:14:51 and here i though b_jonas was your real name 13:23:11 -!- FreeFull has joined. 13:48:33 -!- lollo64it has quit (Ping timeout: 244 seconds). 13:52:56 -!- password2 has joined. 14:16:05 -!- Sorella has joined. 14:27:58 -!- edwardk has joined. 14:37:14 -!- edwardk has quit (Quit: Computer has gone to sleep.). 14:38:42 -!- brandonson has quit (Read error: Connection reset by peer). 14:39:18 -!- brandonson has joined. 14:39:46 -!- brandonson has quit (Read error: Connection reset by peer). 14:40:06 -!- brandonson has joined. 14:42:10 -!- edwardk has joined. 15:07:55 -!- mihow has joined. 15:14:31 -!- Aetherspawn- has quit (Quit: Connection closed for inactivity). 15:34:07 -!- edwardk has quit (Quit: Computer has gone to sleep.). 15:42:03 -!- Phantom_Hoover has joined. 15:46:43 elliott: I don't remember going, I remember coming back 15:48:26 -!- Tritonio has quit (Ping timeout: 240 seconds). 15:53:24 -!- edwardk has joined. 15:58:17 -!- olsner_ has changed nick to olsner. 16:01:17 -!- slereah_ has quit (Quit: Leaving). 16:02:53 -!- edwardk has quit (Ping timeout: 244 seconds). 16:11:59 -!- oerjan has quit (Quit: Yay money). 16:16:10 -!- edwardk has joined. 16:20:58 -!- drdanmaku has joined. 16:54:27 -!- Tritonio has joined. 16:56:04 -!- ^v has changed nick to gabensale2014. 17:17:46 -!- mihow has quit (Quit: mihow). 17:39:24 -!- gabensale2014 has changed nick to ^0. 17:40:05 -!- lollo64it has joined. 17:43:55 -!- MDream has quit (Ping timeout: 272 seconds). 18:08:59 -!- Tritonio has quit (*.net *.split). 18:09:01 -!- edwardk has quit (*.net *.split). 18:09:02 -!- Phantom_Hoover has quit (*.net *.split). 18:09:06 -!- FreeFull has quit (*.net *.split). 18:09:09 -!- contrapumpkin has quit (*.net *.split). 18:09:17 -!- impomatic has quit (*.net *.split). 18:09:19 -!- heroux has quit (*.net *.split). 18:09:44 -!- barrucadu has quit (*.net *.split). 18:09:53 -!- hogeyui_ has quit (*.net *.split). 18:09:55 -!- lifthrasiir has quit (*.net *.split). 18:10:04 -!- idris-bot has quit (*.net *.split). 18:10:33 -!- realzies has quit (*.net *.split). 18:10:34 -!- Gregor has quit (*.net *.split). 18:10:35 -!- monotone has quit (*.net *.split). 18:10:39 -!- augur has quit (*.net *.split). 18:10:48 -!- aloril has quit (*.net *.split). 18:10:49 -!- Slereah has quit (*.net *.split). 18:10:51 -!- HackEgo has quit (*.net *.split). 18:10:58 -!- KingOfKarlsruhe has quit (*.net *.split). 18:11:09 -!- drdanmaku has quit (*.net *.split). 18:11:45 -!- b_jonas has quit (*.net *.split). 18:11:48 -!- shachaf has quit (*.net *.split). 18:11:54 -!- tromp__ has quit (*.net *.split). 18:12:14 -!- MoALTz has quit (*.net *.split). 18:12:15 -!- MindlessDrone has quit (*.net *.split). 18:12:19 -!- Bike has quit (*.net *.split). 18:12:20 -!- sebbu has quit (*.net *.split). 18:12:21 -!- Sprocklem has quit (*.net *.split). 18:12:24 -!- constant has quit (*.net *.split). 18:12:26 -!- TodPunk has quit (*.net *.split). 18:12:32 -!- Melvar has quit (*.net *.split). 18:12:47 -!- nortti has quit (*.net *.split). 18:13:05 -!- kyhwana has quit (*.net *.split). 18:13:09 -!- Burton has quit (*.net *.split). 18:13:15 -!- Taneb has quit (*.net *.split). 18:13:25 -!- ski has quit (*.net *.split). 18:13:50 -!- douglass has quit (*.net *.split). 18:13:54 -!- jix_ has quit (*.net *.split). 18:13:59 -!- diginet has quit (*.net *.split). 18:14:12 -!- ineiros has quit (*.net *.split). 18:14:14 -!- maurer has quit (*.net *.split). 18:14:16 -!- elliott has quit (*.net *.split). 18:14:16 -!- int-e has quit (*.net *.split). 18:14:18 -!- ^0 has quit (*.net *.split). 18:14:26 -!- esowiki has joined. 18:14:30 -!- esowiki has joined. 18:14:31 -!- esowiki has joined. 18:15:13 -!- esowiki has joined. 18:15:14 -!- glogbot has joined. 18:15:17 -!- esowiki has joined. 18:15:18 -!- esowiki has joined. 18:16:25 -!- mihow has joined. 18:16:26 -!- lollo64it has joined. 18:16:26 -!- brandonson has joined. 18:16:26 -!- Sorella has joined. 18:16:26 -!- 17SAAFGOG has joined. 18:16:26 -!- atehwa has joined. 18:16:26 -!- FireFly has joined. 18:16:26 -!- tromp has joined. 18:16:26 -!- coppro has joined. 18:16:26 -!- jj2baile has joined. 18:16:26 -!- myname has joined. 18:16:26 -!- erdic has joined. 18:16:26 -!- `^_^v has joined. 18:16:26 -!- vravn has joined. 18:16:26 -!- Gracenotes has joined. 18:16:26 -!- _46bit has joined. 18:16:26 -!- vyv has joined. 18:16:26 -!- mtve has joined. 18:16:26 -!- clog has joined. 18:16:26 -!- pikhq has joined. 18:16:26 -!- Speed` has joined. 18:16:26 -!- ggherdov has joined. 18:16:26 -!- newsham has joined. 18:17:33 -!- atehwa has quit (Write error: Broken pipe). 18:17:33 -!- 17SAAFGOG has quit (Write error: Broken pipe). 18:17:34 -!- jj2baile has quit (Write error: Broken pipe). 18:32:51 -!- FireFly has quit (Excess Flood). 18:33:08 -!- `^_^v has quit (Excess Flood). 18:33:13 -!- brandonson has quit (Excess Flood). 18:33:32 -!- `^_^v has joined. 18:33:59 -!- brandonson has joined. 18:34:37 -!- FireFly has joined. 19:04:32 -!- shikhin has joined. 19:12:59 -!- ^v has joined. 19:13:53 -!- ^v has quit (Client Quit). 19:31:01 -!- conehead has joined. 19:32:42 -!- Bike has quit (Ping timeout: 245 seconds). 19:34:42 -!- Bike has joined. 19:39:15 -!- MindlessDrone has quit (Quit: MindlessDrone). 19:40:01 `quote midsummer 19:40:01 No output. 19:41:47 `quote night's 19:41:48 No output. 19:41:53 `quote dream 19:41:54 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 19:41:59 `quote fixed pattern 19:41:59 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 19:42:46 `quote 240 19:42:46 240) Gregor, yeah, but Purdue has poultry science facilities beyond the dreams of avarice. 19:44:16 but I did the systembolaget yesterday, 5 minutes before closing when it was empty, so I neatly evaded the queueing 19:48:02 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) 19:48:13 it's also danced to a french march 19:53:03 -!- lifthrasiir has quit (Ping timeout: 240 seconds). 19:57:44 -!- mhi^ has joined. 19:59:00 I like the name "systembolaget". 20:02:32 Can't find the etymology in the (English) 'pedia. 20:02:51 -!- Bike has quit (Ping timeout: 264 seconds). 20:03:14 Our counterpart is just called "Alko", which is very boring. 20:04:20 -!- Bike has joined. 20:04:30 The Norwegian version has a refreshingly direct name. ("Vinmonopolet".) 20:05:27 yeah, exactly what it says, it's pretty nice 20:06:53 "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 20:07:36 it seems that "system" comes from http://en.wikipedia.org/wiki/Gothenburg_Public_House_System 20:07:51 I see. 20:10:32 -!- lifthrasiir has joined. 20:11:07 -!- MDream has joined. 20:11:07 -!- MDream has changed nick to MDude. 20:25:16 applybot: help 20:25:16 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 20:30:30 -!- Frooxius has joined. 20:47:57 -!- Frooxius has quit (Read error: Connection reset by peer). 20:48:52 -!- Frooxius has joined. 21:01:16 -!- Patashu has joined. 21:08:33 -!- oerjan has joined. 21:13:12 -!- nortti has changed nick to lawspeaker. 21:13:32 -!- lawspeaker has changed nick to nortti. 21:13:37 applybot: state 21:13:38 Not in a proof. 21:13:54 fungot: Prove something. 21:13:55 fizzie: src/ ip.h or is it 21:14:15 fungot: ls -lah src 21:14:16 mroman: damn. he got that. but still patch of green where medialab extension is supposed to 21:20:13 -!- Patashu has quit (Disconnected by services). 21:20:13 -!- Patashu_ has joined. 21:23:13 applybot: country 21:23:13 *** Unrecognized command 21:27:00 -!- Patashu_ has quit (Ping timeout: 255 seconds). 21:28:43 -!- Sprocklem has quit (Quit: leaving). 21:29:00 -!- Sprocklem has joined. 21:41:52 applybot: info 21:41:52 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. 21:42:26 applybot: help state 21:42:26 state: Show the state of the current proof (if there is one). 21:43:10 applyvot: context 21:43:22 applybot: help context 21:43:22 context [N]: Show the most recent (N) lines in this session. 21:43:42 applybot context 10 21:43:54 applybot: context 10 21:43:55 Beginning of theory. 21:44:21 applybot: help term 21:44:21 term: Isabelle command 21:44:36 applybot: help Isabelle 21:44:36 Unknown command: Isabelle 21:44:49 applybot: fungot 21:44:49 *** Unrecognized command 21:44:50 MDude: in the matter... things will fnord down after this week hopefully. 21:50:03 -!- boily has joined. 21:50:58 -!- metasepia has joined. 21:51:49 ~duck MSRP 21:51:49 --- No relevant information 21:52:31 -!- edwardk has quit (Quit: Computer has gone to sleep.). 22:02:25 `? b_jonas 22:02:26 b_jonas? ¯\(°​_o)/¯ 22:02:46 an sudden opportunity appears! b_jonas, how would you wisdomically describe yourself? 22:04:09 [wiki] [[AlphaBeta]] http://esolangs.org/w/index.php?diff=39860&oldid=34593 * 188.192.76.116 * (+257) Added Lua implementation from Michael Armbruster 22:10:25 -!- nooodl has joined. 22:28:45 -!- boily has quit (Quit: INDIAN CHICKEN). 22:28:47 -!- metasepia has quit (Remote host closed the connection). 22:39:27 -!- Phantom_Hoover has quit (Ping timeout: 255 seconds). 22:42:39 -!- Phantom_Hoover has joined. 22:55:26 -!- Sgeo has joined. 23:09:31 ~duck help 23:09:49 ~duck metasepia 23:10:13 -!- ^v has joined. 23:10:15 Oh, metasepia has left. 23:11:35 `? metasepia 23:11:36 metasepia knows the weather at your nearest airport, and also something about ducks. 23:13:28 `? MDude 23:13:29 MDude? ¯\(°​_o)/¯ 23:13:52 `learn MDude is just a dude, with an M's courage. 23:13:54 I knew that. 23:17:47 are you sure he's not a million dudes 23:20:04 -!- ^v has quit (Quit: http://i.imgur.com/Akc6r.gif). 23:21:33 That would be pretty cool. 23:22:22 Who was that person in B who blatantly had no idea about anything in the rules? 23:22:57 I don't know what B is, so if I was in it I clearly had no idea. 23:23:30 `? B 23:23:31 B? ¯\(°​_o)/¯ 23:23:41 I think that serves as proof that MDude was that person in B 23:24:34 It's pretty strong evidence. 23:24:42 -!- ^v has joined. 23:29:08 M P Darke 23:33:27 -!- Phantom_Hoover has quit (Ping timeout: 264 seconds). 23:37:26 -!- shikhout has joined. 23:40:12 -!- shikhin has quit (Ping timeout: 245 seconds). 23:45:14 -!- mihow has quit (Quit: mihow). 23:55:40 argh i now have _four_ tabs with shtetl-optimized comment threads open that i haven't managed to finish... 23:56:38 (even once. i sometimes go back to old ones to check for new comments.) 23:57:30 Is that F# monad tutorial that doesn't say 'monad' about monads in general or just the Error monad? 23:58:03 it's really a thinly disguised burrito cookbook hth 23:59:18 http://www.calcentral.com/~monadrailway/Monad/Welcome.html