00:00:26 oerjan: file uses magic 00:00:35 -!- mb06cs has joined. 00:00:46 ic 00:00:51 -!- Vacation9 has joined. 00:00:59 -!- Vacation9 has left ("Konversation terminated!"). 00:01:10 o_o 00:01:38 this vacation9 person, seems to have a lot of trouble 00:01:52 elliott: well file doesn't recognize the first encoding as anything other than ASCII text 00:01:58 -!- carado has quit (Remote host closed the connection). 00:02:11 *outermost 00:03:16 That's something anyone doing this kind of stupid-day puzzle does, though. 00:03:52 well in that case they'll do all the rest too :P 00:04:26 -!- carado_ has joined. 00:04:32 or wait was that to Bike 00:04:54 oh, Sgeo is also there 00:04:54 I don't think people in general eyeball the second one, though. Maybe. 00:05:10 oerjan: No, it was to you. 00:05:41 Having done a bit of the official one, I can't really be criticizing anyone else for wasting their time. 00:06:17 nooga, elliottcable invited me there after I ranted a bit about node.js in the node.js channel 00:06:29 Bike: shachaf: i'm pretty sure that periodic function stuff is trivial if you can use the axiom of choice (and thus get a basis for the reals as a rational vector space), but is that intended? 00:06:44 oerjan: given the context, probably. 00:07:03 Sgeo: oh, I didn't know you're into node 00:07:16 I'm not into node 00:07:25 no? 00:07:33 de 00:07:36 then what were you doing in the #node.js? 00:08:38 good question 00:08:53 -!- kallisti has quit (Ping timeout: 255 seconds). 00:09:01 Complaining about node 00:09:02 Hey, what am I doing on #esoteric? Are people going to think I'm... into it? 00:09:12 indeed 00:09:15 you are 00:10:10 fizzie: they might start thinking you do wacky things such as programming befunge 00:10:45 7part #esoteric OH NOOOOO 00:11:50 also it is trivial that the two functions cannot be continuous, since then they would be bounded. 00:12:03 Sgeo: Did you seriously join #node.js to talk about how node.js is bad? 00:12:18 Yes 00:12:20 >.> 00:12:28 When people do that in #haskell, we usually consider them annoying trolls. 00:13:19 surely there is #haskell-flames for that. 00:13:28 Hi all. Esoteric programming languages are bad. 00:13:34 -!- ChanServ has set channel mode: +o oerjan. 00:13:47 -!- oerjan has kicked ion Fuck off and die. 00:13:52 -!- oerjan has set channel mode: -o oerjan. 00:14:03 ion was kicked from #esoteric by oerjan [Fuck off and die] 00:14:05 golden 00:14:23 oerjan actually typed the F word 00:14:30 Good to see someone showing those uppity trolls who's the boss. 00:14:46 -!- ion has joined. 00:14:51 goljan oerden 00:14:51 `pastelogs WRONG WITH YOU 00:15:01 nooga: i'm sure it's happened before 00:15:39 http://codu.org/projects/hackbot/fshg/index.cgi/raw-file/tip/paste/paste.31028 00:16:09 Precedent! 00:16:19 imo oerjan is abusing his op powers 00:16:21 imoerjan 00:17:09 emoerjan 00:17:21 Instant Messagerjan. 00:17:48 shachaf: i vaguely recall you were being quite annoying. 00:18:22 although possibly by accident. 00:18:59 oerjan: irc.dahl.net 00:19:22 Oh nohl. 00:19:26 -!- nooga has changed nick to Meldo. 00:19:32 -!- Meldo has changed nick to nooga. 00:19:38 ...now i remember. maybe i should kick you again. 00:19:59 :☹( 00:20:12 Not a fan of Roald Dahl? 00:20:17 `run echo kick|h 00:20:19 kihck 00:24:19 kicques 00:25:16 oerjan: Why do you hate dahl.net so much? 00:25:21 http://overviewer.org/ 00:26:17 shachaf: because it doesn't exist. 00:26:30 A kihck graph is formed by taking all the maximal kihcks (people who've each kihcked each other) on the original channel, and adding an edge if the "F word" was used in a cross-maximal-kihck kihck event. 00:27:55 OHKAY 00:29:27 (Is there a sort of a clihque for directed graphs?) 00:30:31 probably several kinds 00:31:54 Assuming the kind where directions are removed and multiple edges collapsed, are there maximal kihcks on #esoteric larger than two? 00:32:33 That's the kind of question I'd like to ask W|A but I think they still haven't "curated" data about #esoteric. 00:32:35 rip ibm roadrunner 00:33:11 let's code some node 00:33:36 beep beep 00:33:56 "Meep meep", isn't it? 00:34:01 * Sgeo suddenly remembers that Bike wants to see a video of him typing. 00:34:36 fizzie: i'm pretty sure you are the most qualified person to collect and visualize the data hth 00:34:48 I... do? 00:34:52 Oh right, because you don't touch type. 00:35:35 fizzie: wikipedia seems to insist on beep 00:35:41 oerjan: It's like 3:35am and I was just going to sleep, and then you say something like that. "H", indeed. 00:36:02 SORRRY 00:36:22 I seem to have been wrong on the meeps too. 00:36:39 also http://answers.yahoo.com/question/index?qid=20070608064934AAlD3Rb 00:38:10 (warning: that was about as depressing as you'd expect) 00:41:37 -!- augur has joined. 00:45:57 -!- ssue_ has joined. 00:58:22 -!- augur has quit (Remote host closed the connection). 01:03:20 -!- augur has joined. 01:07:41 https://dl.dropbox.com/u/113389132/Misc/20130401-kick.png well now THAT was quite something. 01:08:12 elliott's been very bad. 01:08:38 youguysaremean / IWontSayAWord / pleasehearmeout <-- omg 01:08:43 The line thickness is from the count. 01:08:47 fizzie: can you... make this vertical instead 01:09:02 -!- Taneb has quit (Quit: Leaving). 01:09:03 elliott: Possibly with a rankdir=LR. 01:09:44 https://dl.dropbox.com/u/113389132/Misc/20130401-kick2.png same thing the other way around. 01:10:45 As far as graphs go, it's remarkably bipartite. 01:10:54 With the self-edges being the only exceptions. 01:11:02 fizzie: you should op me so i can add some data to it. 01:11:06 I bet Bike wants to be kicked for science. 01:11:41 fizzie: i see tusho and lament kicked each other. i think. 01:11:55 oerjan: As did you and elliott, somehow. 01:12:14 oh. that wasn't visible. 01:12:26 It's more visible in the vertical version. 01:12:28 i also kicked monqy! 01:12:30 -!- nooga has quit (Ping timeout: 245 seconds). 01:12:30 Since it's bipartite, it also means my original question about maximal kihcks of size greater than two probably has a negative answer. 01:12:53 anyway c'mon. opping me so i can kick people for fun is practically a tradition by now. 01:13:17 Nooo, I'll go a sleep now byebye -> 01:13:28 ok i guess oerjan has to do it then 01:15:27 fizzie: you are _quite_ a lazy op hth 01:17:01 it's awful. i'll kick him for it 01:20:15 oerjan: wow I feature deadfish and don't even get anything in return! 01:20:20 `run dmesg | paste 01:20:24 http://codu.org/projects/hackbot/fshg/index.cgi/raw-file/tip/paste/paste.13850 01:20:49 `slist 01:20:51 slist: Taneb atriq Ngevd Fiora nortti Sgeo ThatOtherPerson alot 01:20:54 `run dmesg | tac 01:20:55 ubda: unknown partition table \ console [mc-1] enabled \ Initializing software serial port version 1 \ console [tty0] enabled \ Console initialized on /dev/tty0 \ Initialized stdio console driver \ sit: IPv6 over IPv4 tunneling driver \ NET: Registered protocol family 10 \ TCP: cubic registered \ loop: module loaded \ brd: module loaded \ io sc 01:21:54 is tusho elliott or tswett, i always confuse it with kerlo 01:22:06 http://www.intercaloninterstates.org/ oh geez 01:22:06 it's NSQX 01:22:24 no it's not hth 01:22:27 Fiora: heh 01:22:48 wow it actually has sample code 01:23:24 yay the readme links to our wiki 01:24:29 (I finally found a relevant link for like once in forever) 01:25:40 more often than most of us manage 01:26:58 oerjan: http://ro-che.info/articles/2013-03-31-flavours-of-free-applicative-functors.html 01:27:02 oerjan: congratulations on being /r/haskell famous 01:27:09 albeit with a low-fidelity rendering of your name 01:28:10 I hit 110 pounds! 01:28:25 congrats 01:28:28 how tall are you Sgeo? 01:29:01 5'2" (around there, maybe a bit taller, I forget, 5'2" to 5'4" or so) 01:29:35 Jesus you're short. 01:29:38 elliott: argh i think he missed half the point, which was that my implementation doesn't use Functor f... 01:29:46 oerjan: the functor f thing is mentioned later. 01:29:51 oh. 01:29:59 oerjan: then he says you're a cannon! 01:30:06 eek 01:33:18 `run ls -l /dev/ubd* 01:33:20 ls: cannot access /dev/ubd*: No such file or directory 01:34:02 `paste < /tmp/16551.conf 01:34:04 http://codu.org/projects/hackbot/fshg/index.cgi/raw-file/tip/%3C%20/tmp/16551.conf 01:34:17 er 01:34:19 `run paste < /tmp/16551.conf 01:34:21 bash: /tmp/16551.conf: No such file or directory 01:34:24 :( 01:35:04 5'2" isn't that short! 01:35:18 and congrats :o 01:35:47 Thanks 01:36:03 Pretty much everyone else I know who is this short is female 01:36:38 I don't entirely understand why so many women are short compared to men 01:36:39 I guess that's true, the average for guys is like 5'9" or something 01:36:50 I think it's just sexual dimorphism? 01:37:22 i feel like i should say "sexual dimorphism" winkingly and then transmute myself into a horrid fleshbeast 01:37:37 pfff:p 01:38:15 elliott: yay 01:39:22 Bike: aren't you already a horrid fleshbeast 01:40:04 Well I mean moreso. 01:40:07 Since I'd be a sexual one. 01:40:22 Hawt. 01:40:33 a terrified, asexual forcemeat 01:40:44 `addquote i feel like i should say "sexual dimorphism" winkingly and then transmute myself into a horrid fleshbeast 01:40:47 1004) i feel like i should say "sexual dimorphism" winkingly and then transmute myself into a horrid fleshbeast 01:41:04 sexual animorphism 01:41:24 Jesus you're short. // actually, given the change of humans' height over time, yeah, he's probably about as tall as Jesus was. 01:41:47 wait who's the asexual fleshbeat 01:42:15 truly, aren't we all asexual fleshbeasts. 01:44:47 elliott: he actually asked me in a message if i wanted to give my real name for attribution, but i haven't got around to visiting reddit properly yet today 01:44:58 Afraid I'm a sexual fleshbeast. 01:45:09 so i just saw it when clicking on the link back from the blog post to reddit 01:45:38 Örjan 01:47:13 a porn version of the animorphs 01:48:09 Sexual polymorphism 01:55:53 -_- 01:59:19 -!- mb06cs has quit (Ping timeout: 246 seconds). 02:00:05 i feel i've seen better wikipedia front pages for this date than this. 02:01:20 WE ARE NOT AMUSED 02:02:19 lame featured article 02:02:38 yeah that was the worst 02:03:25 today's picture was the best i think 02:03:38 -!- mb06cs has joined. 02:03:52 wikipedia has a front page? 02:04:12 the front page is /wiki/Special:Search?search=, right? 02:04:20 and the rest was trying to stretch things too far to try and be humorous 02:04:27 no, shachaf 02:04:56 oh 02:04:59 thoerjan 02:05:07 ywachaf 02:06:00 *to 02:06:11 oerjan: imo that works better with rwbarton 02:06:40 okachaf 02:21:22 oerjan: tusho is elliott. 02:21:45 -!- mb06cs has quit (*.net *.split). 02:21:46 -!- carado_ has quit (*.net *.split). 02:21:46 -!- myndzi has quit (*.net *.split). 02:21:53 you can't hide, NSQX. 02:22:04 -!- alex_joni has joined. 02:22:18 Bike: looks like we need more clues. 02:22:38 help how do i write \mathcal letters on paper 02:25:15 -!- FreeFull_ has joined. 02:25:28 -!- FreeFull has quit (Write error: Broken pipe). 02:26:14 nooodl_: pretend you're 19th century european royalty. 02:26:29 haha that's actually pretty much what i'm doing 02:26:36 they're so swooshy and unreadable... god 02:27:00 i'll just write a bunch of As Bs and Cs and hope i never have to deal with anything beyond that 02:27:18 alex_joni: What's a function that's continuous almost everywhere but differentiable nowhere? 02:28:04 Why almost? 02:28:16 indeed, drop the almost. 02:28:25 Maybe Bike is thinking of a different function. 02:28:33 `welcome alex_joni 02:28:35 alex_joni: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: http://esolangs.org/wiki/Main_Page. (For the other kind of esoterica, try #esoteric on irc.dal.net.) 02:30:42 how do i keep misplacing all of my virtual machines 02:30:48 -!- alex_joni has left ("later"). 02:31:36 everyone i love dies :( 02:31:57 :/ 02:32:43 s/i love // hth 02:32:55 oerjan: Bike loves everyone 02:33:25 Yes. 02:35:54 -!- augur has quit (Remote host closed the connection). 02:38:32 -!- augur_ has joined. 02:38:50 -!- mb06cs has joined. 02:38:50 -!- carado_ has joined. 02:38:50 -!- myndzi has joined. 02:39:50 Bike: alex_joni: What's a function that's continuous almost everywhere but differentiable nowhere? 02:40:22 all functions! 02:40:32 what 02:40:33 * Koen_ in Koen's world, all sets are discrete 02:40:50 ok 02:41:09 Isn't it the same in elliott's world. 02:41:15 isn't there one that's like... f(p/q) = 1/q, f(x) = 0 for p,q integers, x irrational 02:41:24 weierstrass's is the "canonical" one 02:41:32 i think elliott believes in differentiable functions 02:42:31 fractalicious 02:42:46 while we're talking about weird functions, i like http://en.wikipedia.org/wiki/Conway_base_13_function 02:43:03 -!- Sgeo has quit (Excess Flood). 02:43:44 My favorite conway thing is probably that huge-ass polynomial. 02:43:50 -!- Sgeo has joined. 02:44:13 the one for look-and-say. 02:46:25 -!- augur_ has quit (Remote host closed the connection). 02:49:32 -!- glogbackup has quit (*.net *.split). 02:50:07 i haven't sen 02:50:09 seen 02:50:19 seen what 02:50:36 that polynomial 02:50:38 Conway's huge polynomial? Hereabouts it is: http://en.wikipedia.org/wiki/Look-and-say_sequence 02:50:52 Yeah, it's in there, like degree 70-something 02:51:21 -!- augur has joined. 02:52:39 kmc: how is that continuous? 02:52:55 you're jumping from 1/q to 0 02:53:38 Koen_: as you get closer to an irrational number by rational approximations, the denominator gets bigger and bigger 02:54:24 I bet you can't find a rational that's right next to an irrational. 02:55:50 oh 02:55:52 ok 02:55:53 -!- augur has quit (Ping timeout: 258 seconds). 02:56:12 help what's a right next to 02:56:42 I think the usual term is equality 02:57:29 shachaf: Right. 02:58:07 -!- monqy has joined. 02:59:25 hi monqy 02:59:30 hi 02:59:31 monqy: You have 1 new message. '/msg lambdabot @messages' to read it. 02:59:49 got you! 02:59:58 Oh boy. Conway's base 13 function takes on the value of every real number, in every open interval? 02:59:58 -!- aytch has joined. 03:00:04 wait that wasn't even my @message 03:00:40 -!- aytch has left ("Leaving..."). 03:00:40 oh, that's a good property. 03:00:41 doesn't identity do that already? 03:00:41 I want to have a lambdabot message. 03:00:54 oh wait 03:01:07 @tell tswett Not a chance 03:01:07 Consider it noted. 03:01:09 maybe not then 03:01:22 hey oerjan this article talks about someone who shares your first name 03:01:27 what are the chances 03:01:45 shachaf: infinitesimal 03:03:28 I regard Oerjan’s version as the principal one. It is simple, powerful (doesn’t require f to be a functor) and straightforward (doesn’t change the arguments order). 03:03:46 "doesn’t require f to be a functor"? 03:03:46 So what's the best function that takes on every value on every interval? 03:03:46 tswett: You have 1 new message. '/msg lambdabot @messages' to read it. 03:04:00 *gasp* I have a message? :Ö: 03:04:14 @messages 03:04:15 oerjan said 3m 8s ago: Not a chance 03:04:42 I'm so happy. :'))))))))))))))))))))))))))))))))) 03:05:07 tswett: that base 13 function does look pretty good 03:06:01 shachaf: nope, it doesn't 03:06:20 `slist 03:06:21 slist: Taneb atriq Ngevd Fiora nortti Sgeo ThatOtherPerson alot 03:06:23 [S] 03:06:35 oerjan: What about all these "Functor f =>" constraints? 03:06:55 shachaf: completely redundant 03:06:58 -!- Bike_ has joined. 03:07:04 -!- augur has joined. 03:07:08 -!- augur has quit (Remote host closed the connection). 03:07:11 Anyway I'm not sure what it means for it to be a "free applicative" if there's no functor. 03:07:47 shachaf: the applicative itself is a functor. it just doesn't use any underlying one. 03:07:59 Right. 03:08:12 So what is it a "free applicative" of? 03:08:23 Well... In what sense is it "free"? 03:08:30 of a * -> * kind data constructor 03:08:41 Well, sure. 03:08:45 what does "free" even mean help 03:09:27 well usually it's about having the right universal property 03:09:59 -!- Bike has quit (Ping timeout: 240 seconds). 03:10:06 i thought "free" meant "left adjoint to a forgetful functor" or something 03:10:17 shachaf: that "lower" function should probably be the corresponding forgetful functor 03:10:24 -!- Bike_ has changed nick to Bike. 03:12:13 or part of it 03:13:56 -!- augur has joined. 03:14:26 -!- augur has quit (Remote host closed the connection). 03:15:44 -!- heroux has quit (Ping timeout: 256 seconds). 03:17:07 -!- heroux has joined. 03:18:23 oerjan: Can you explain the thing with the free F-Alg monad? 03:19:16 no. 03:19:54 i haven't been following those posts 03:20:20 Which posts? 03:20:27 This is unrelated to ro-che. 03:21:14 well i vaguely recall seeing reddit posts mentioning F-algebras 03:21:41 WELL I'M NOT TALKING ABOUT THOSE REDDIT POSTS 03:21:50 (unless i actually am talking about them) 03:22:11 well i'm pointing out i haven't learned anything about F-algebras 03:22:43 i may have had my eyes glaze over over some of those posts, that's all 03:26:03 I guess copumpkin will have to explain it. 03:26:40 wat 03:28:12 copumpkin: i categorically refused to answer, so you will have to answer categorically. 03:28:37 oerjan++ 03:37:01 Has Google Maps had this "Treasure" mode for a while or is it an April thing? 03:37:42 latter aiui 03:43:31 huh, seems like quite a bit of effort to do, I think? 03:43:40 I don't know, I don't know how image processing works 03:44:13 Hmm, probably not 03:45:01 It's all done by hand. 03:45:38 are you saying humans have developed the technology to "draw" "maps" 03:47:27 they use wood and arrows 03:49:06 elliott: sheesh elliott, humans made maps even in the middle age. it just took them most of their life to complete one. 03:49:26 oerjan: ummm they didn't have image processing technology in the middle ages 03:50:44 elliott: that's why it took so long to make, duh 03:50:56 they had to do it without processing. 03:50:59 * Sgeo was thinking at first that Google was taking the rendered map image and converting it to treasure, but presumably Google actually has map data which makes more sense 03:58:16 -!- nooodl_ has quit (Ping timeout: 272 seconds). 04:01:35 They didn't even have aircraft back then; how could they have had maps? 04:03:32 -!- nooodl has joined. 04:09:36 -!- augur has joined. 04:11:27 -!- ousia has joined. 04:21:04 -!- oerjan has quit (Quit: Gnäyt). 04:21:18 -!- nooodl has quit (Ping timeout: 252 seconds). 04:24:39 -!- glogbackup has quit (Remote host closed the connection). 04:26:20 oh yeah, f-algebras 04:26:27 world's most boring concept 04:29:57 -!- sathiyac2 has joined. 04:29:59 That's pretty boring. 04:30:46 take an endofunctor F 04:30:52 on category C 04:31:07 F-algebra is an object x of C and a morphism from F x -> x 04:31:10 there you go 04:31:14 no laws, no nothing 04:31:28 OK. 04:31:33 why do you need an endofunctor? 04:31:34 Why do free F-algebras give you free monads? 04:31:42 wait, never mind 04:31:48 elliott: badly typed otherwise :) 04:31:54 :-X 04:32:00 copumpkin: It could be a contravariant functor! 04:32:09 sathiyac2: :-Y 04:32:20 sathiyac2: Try unzipping it. 04:32:24 shachaf: it could be, not sure what would happen to the category construction then 04:32:43 Anyway this is apparently very related to free monads. 04:32:50 shachaf: not sure about a free f-algebra 04:33:04 you know how you get data out of initial f-algebras though? 04:33:23 initial and free are kinda similar 04:33:26 "out of"? 04:33:29 Do you mean using? 04:33:31 well, how they're connected 04:33:37 or how one is justified by the other 04:34:29 That's related to foldr with (:) and [], I guess? 04:34:43 yeah, or folds in general 04:34:51 Right. 04:34:55 can u plz tell me . . wat is f-algebra ? 04:34:56 which are just defining characteristics of data 04:35:12 sathiyac2: 05:30:46 take an endofunctor F 04:35:13 05:30:53 on category C 04:35:13 05:31:07 F-algebra is an object x of C and a morphism from F x -> x 04:35:13 But I'm not sure what you mean in particular. 04:35:15 anyway, it turns out that f-algebras can be made into a category 04:35:27 so for a particular F, you can construct its category of F-algebras 04:35:45 where the algebras are objects, and the morphisms are still pretty simple 04:37:06 so basically I said that an f-algebra is an object of C and a morphism in it. To look at the moprhism between two f-algebras, just take a moprhism between their two objects, such that a fairly obvious law is satisfied 04:37:28 so anyway, now you have this category of f-algebras 04:37:41 if you look at the initial obejcts in that category, you'll find you can prove a remarkable property about them 04:37:45 which is called lambek's lemma 04:39:07 The morphism part of every initial F-algebra has an inverse? 04:39:16 well sort of 04:39:47 but the more interesting part is that the object part X of that initial algebra is isomorphic to F X 04:39:52 so X ~= F X 04:40:20 which is basically a roundabout way to get a fixed point 04:40:47 Well, that's the same thing, isn't it? If f : F X -> X has an inverse then X ~= F X? 04:40:55 sure 04:41:14 OK. Hmm. 04:41:25 I just think phrasing it as a fixed point is more revealing 04:41:41 when we're used to writing data ListF a r = …; Mu (ListF a) 04:41:48 Right. 04:42:46 the same argument works for terminal coalgebras of course 04:42:49 and gets you codata 04:43:38 oh shit, the fake announcements have already started popping up 04:44:13 So the free monad thing is related, I think. 04:44:36 For the left adjoint to the forgetful functor : F-Alg(C) -> C 04:45:21 -!- btiffin has joined. 04:46:30 That works out to be the same as the free monad? 04:48:22 beats me :) 04:48:24 work it out 04:48:28 I'm going to sleep! 04:48:42 what is this "work" thing.......... 04:48:47 copumpkin: Thanks! 04:49:02 lol 04:49:03 Now I know a bit about Lambek's Lemma and Colambek's Colemma. 04:49:10 I have work to go to tomorrow! 04:49:15 can't stay up all night doing CT, you know 04:49:20 such is life in CT 05:02:24 what is metasploit can u plzz 05:02:51 can u plz. 05:03:00 no Bike. plzz. 05:03:11 what is lmgtfy 05:03:42 am new dont mistake mee frnds 05:04:20 `relcome sathiyac2 05:04:23 sathiyac2: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: http://esolangs.org/wiki/Main_Page. (For the other kind of esoterica, try #esoteric on irc.dal.net.) 05:23:22 -!- carado_ has quit (Ping timeout: 246 seconds). 05:25:55 copumpkin: class Algebra a where algebra :: F a -> a 05:26:17 newtype Foo a = Foo { runFoo :: forall r. Algebra r => (a -> r) -> r } 05:27:25 no restriction on F? 05:27:39 F is a specific functor. 05:27:49 You can tell because it's uppercase. 05:27:54 oh. 05:28:53 With MPTCs you can say class Algebra f a where ... 05:33:29 -!- sathiyac2 has left. 05:37:12 Has anyone tried CB Slang syntax? 05:37:50 10- codes? 05:37:50 like cb radio? 05:37:55 yep 05:38:01 10-4 good buddy 05:39:09 Just curious. 05:51:57 oh interesting. ML was introduced to write tactics for LCF. 05:52:13 so the OCaml and Coq thing just continues that trend of ML-family languages being invented for theorem provers... 05:53:51 cute 06:05:30 -!- sebbu2 has joined. 06:06:09 -!- sebbu2 has quit (Changing host). 06:06:09 -!- sebbu2 has joined. 06:07:02 monqy: maybe you feel like talking about the f-algebra thing a bit 06:07:24 um 06:07:25 ??? 06:08:03