00:00:03 -!- erdic has quit (Changing host). 00:00:03 -!- erdic has joined. 00:01:44 -!- boily1 has joined. 00:02:08 -!- tromp__ has joined. 00:02:25 -!- atehwa has joined. 00:03:03 -!- Slereah__ has joined. 00:03:28 It timed out, and now it’s in a different net fragment. 00:04:20 ~duck melvar 00:04:20 General Melvar was the right hand man of Warlord Zsinj. 00:04:32 ~duck Taneb 00:04:32 --- No relevant information 00:04:33 :( 00:04:43 ~duck University of York 00:04:43 The University of York (informally York University, or simply York, abbreviated as Ebor. 00:05:15 ebor? 00:05:25 Short for Eboracum, I presume 00:05:42 Roman name for York 00:05:57 -!- sgeoweb has joined. 00:06:02 ~duck eboracum 00:06:02 Eboracum was a fort and city in Roman Britain. 00:06:06 hi. afk 00:06:56 -!- variable has joined. 00:07:00 as the proverb goes, "Anas non satis accurate in hac nocte..." 00:07:36 -!- idris-ircslave has joined. 00:07:36 -!- trn has joined. 00:07:36 -!- Frooxius has joined. 00:08:16 -!- trn has quit (Max SendQ exceeded). 00:08:19 -!- nortti_ has joined. 00:08:32 ( :t getWitness 00:08:32 getWitness : (Exists a P) -> a 00:08:37 ( :t getProof 00:08:37 getProof : (s : Exists a P) -> P (getWitness s) 00:10:50 -!- sebbu has quit (Ping timeout: 246 seconds). 00:10:52 -!- idris-ircslave has changed nick to 23LAATE3Q. 00:10:52 -!- idris-ircslave has joined. 00:10:52 -!- atehwa_ has quit (Ping timeout: 246 seconds). 00:10:52 -!- elliott_ has quit (Ping timeout: 246 seconds). 00:10:52 -!- boily has quit (Ping timeout: 246 seconds). 00:10:52 -!- glogbackup has quit (Ping timeout: 246 seconds). 00:10:56 -!- idris-ircslave has quit (Client Quit). 00:10:56 -!- nortti has quit (Ping timeout: 246 seconds). 00:10:56 -!- itsy has quit (Ping timeout: 246 seconds). 00:10:56 -!- Slereah_ has quit (Ping timeout: 246 seconds). 00:10:56 -!- tromp has quit (Ping timeout: 246 seconds). 00:10:56 -!- trn has joined. 00:10:56 o.o 00:11:01 bye for now 00:11:08 -!- sgeoweb has quit (Quit: Page closed). 00:11:15 -!- boily1 has changed nick to boily. 00:11:21 -!- Froox has joined. 00:12:00 quousque tandem abutere, boily, latina nostra? 00:12:22 -!- tromp_ has quit (Remote host closed the connection). 00:12:41 -!- FireFly has joined. 00:12:49 -!- 23LAATE3Q has quit (Ping timeout: 240 seconds). 00:13:09 are we being ddosed again 00:13:39 -!- Frooxius has quit (Ping timeout: 240 seconds). 00:14:50 -!- Sgeo_ has quit (Ping timeout: 265 seconds). 00:14:55 Taneb: “How long, pray will you abuse boily, the Latin do with us?” ← uhm... wut? 00:15:10 oerjan: thausibly. 00:15:15 -!- Sgeo has joined. 00:15:31 boily, ? 00:15:33 i just changed a couple words in an _actual_ famous quote fwiw 00:15:58 Taneb: I can't read. I meant to answer oerjan. 00:16:04 Okay 00:16:07 (stupid term colours.) 00:16:13 fancy 00:16:23 Wouldn't be "our Latin"? 00:17:06 I don't do the Latin. you can get addicted to it! 00:17:11 https://en.wikipedia.org/wiki/Catiline_Orations#Oratio_in_Catilinam_Prima_in_Senatu_Habita 00:17:45 Taneb: i assume he tried google translate 00:18:22 Anyway, I have a nine o'clock train. Goodnight 00:18:38 bonne nuitaneb! 00:18:47 good night 00:19:26 :) 00:21:29 -!- erdic has quit (Remote host closed the connection). 00:27:02 -!- erdic has joined. 00:31:57 -!- yorick has quit (Read error: Connection reset by peer). 00:44:53 -!- FireFly has quit (Excess Flood). 00:46:11 -!- FireFly has joined. 00:55:17 -!- elliott has joined. 00:55:26 -!- elliott has quit (Client Quit). 00:55:41 -!- elliott has joined. 00:59:15 -!- tromp has joined. 01:02:41 -!- metasepia has quit (Remote host closed the connection). 01:02:47 -!- boily has quit (Quit: GALAPAGOS CHICKEN). 01:16:17 -!- erdic has quit (Remote host closed the connection). 01:16:51 -!- erdic has joined. 01:21:32 -!- ^v has joined. 01:27:00 beware of the topic 01:27:05 -!- conehead has quit (Quit: Computer has gone to sleep.). 01:34:33 The risk is merely topical. 01:34:59 well but it's particularly high today (tomorrow for you americans) 01:48:05 -!- Slereah_ has joined. 01:49:43 -!- Slereah__ has quit (Ping timeout: 264 seconds). 02:05:49 -!- conehead has joined. 02:06:00 -!- tromp has quit (Remote host closed the connection). 02:06:35 -!- tromp has joined. 02:10:56 -!- tromp has quit (Ping timeout: 264 seconds). 02:20:07 -!- oerjan has quit (Quit: Nite). 02:22:51 Et tu, oerjan? 02:27:50 -!- tromp has joined. 02:40:16 -!- Slereah__ has joined. 02:42:08 -!- Slereah_ has quit (Ping timeout: 264 seconds). 02:45:40 -!- nooodl has joined. 02:47:24 -!- nooodl__ has quit (Ping timeout: 255 seconds). 02:51:18 -!- Sellyme has quit (Excess Flood). 02:53:55 -!- Sellyme has joined. 03:10:49 ) 1 + 1 03:10:49 Sgeo: 2 03:10:52 ( 1 + 1 03:10:56 :( 03:12:16 ^bf +>+[-<+>]<. 03:12:16 03:21:03 -!- conehead has quit (Quit: Computer has gone to sleep.). 03:32:31 17:14:05 --- nick: idris-ircslave -> 23LAATE3Q 03:32:34 What was that about? 03:37:25 -!- Slereah_ has joined. 03:39:08 -!- Slereah__ has quit (Ping timeout: 264 seconds). 03:40:56 -!- nooodl has quit (Ping timeout: 264 seconds). 03:46:07 -!- tromp has quit (Remote host closed the connection). 03:46:40 -!- tromp has joined. 03:50:51 -!- tromp has quit (Remote host closed the connection). 03:51:05 -!- tromp has joined. 03:51:31 -!- Guest95255 has quit (Quit: Connection closed for inactivity). 03:54:55 -!- Slereah__ has joined. 03:57:08 -!- Slereah_ has quit (Ping timeout: 264 seconds). 04:01:10 -!- shikhout has joined. 04:04:15 -!- shikhin has quit (Ping timeout: 255 seconds). 04:04:16 -!- shikhout has changed nick to shikhin. 04:10:07 -!- Sorella has quit (Quit: It is tiem!). 04:45:49 -!- tromp has quit (Remote host closed the connection). 04:45:56 Sgeo: Bogosity due to netsplits and -joins. 04:46:25 -!- tromp has joined. 04:48:50 -!- nisstyre_ has joined. 04:51:08 -!- tromp has quit (Ping timeout: 264 seconds). 04:55:05 -!- idris-ircslave has joined. 04:56:00 ( the (a ** b) (5 ** "hi") 04:56:01 (input):1:11:No such variable b 04:56:20 ( the (a ** String) (5 ** "hi") 04:56:20 (5 ** "hi") : (a ** String) 04:59:04 -!- variable has changed nick to trout. 05:04:41 wat 05:06:36 A dependent pair where the proof's type isn't actually dependent on the witness 05:07:48 Almost wish you could do useful things with Types, make (t ** t) effectively be the typed of runtime-tagged values, practically dynamic typing 05:08:11 ( the (t ** t) (Int ** 5) 05:08:14 (Int ** 5) : (t ** t) 05:11:10 Totally useless but heterogeneous vector 05:12:25 > the (Vect 3 (t ** t)) $ [(Int ** 5), (String ** "Hello"), ((a -> a) ** id)] 05:12:27 Not in scope: `the'Not in scope: data constructor `Vect'Not in scope: data c... 05:12:27 (input):1:61:No such variable a 05:12:27 Perhaps you meant one of these: 05:12:27 `In' (imported from Lambdabot.Plugin.Haskell.Eval.Trusted), 05:12:27 `InR' (imported from Lambdabot.Plugin.Haskell.Eval.Trusted)Not in scope: d... 05:12:29 oops 05:12:51 ( the (Vect 3 (t ** t)) $ [(Int ** 5), (String ** "Hello"), (({a : Type} -> a -> a) ** id)] 05:12:53 (input):1:25: error: expected: operator 05:12:53 the (Vect 3 (t ** t)) $ [(Int ** 5), (String ** "Hello"), (({a : Type} -> a ->> 05:12:53 ^ 05:13:15 ( the (Vect 3 (t ** t)) $ [(Int ** 5), (String ** "Hello"), (((a : Type) -> a -> a) ** the)] 05:13:22 [(Int ** 5), (String ** "Hello"), ((a124 : Type) -> a124 -> a124 ** the)] : Vect 3 (t ** t) 05:13:44 Sgeo: I was mostly puzzled by the unconstrained a variable 05:14:10 Implies implicit argument 05:14:14 I believe 05:14:19 Although ** is syntax sugar 05:16:51 [00:56:20] (5 ** "hi") : (a ** String) 05:16:54 that 05:17:14 ( :t 5 05:17:14 fromInteger 5 : Integer 05:17:19 ( :t 5 : a 05:17:19 (input):1:1: error: expected: end of input, 05:17:19 operator 05:17:19 :t 5 : a 05:17:19 ^ 05:17:20 parse error (possibly incorrect indentation or mismatched brackets) 05:17:22 ( :t the a 5 05:17:22 (input):1:8:No such variable a 05:17:37 oh I see 05:17:39 it's a binder 05:17:56 wait, is it? 05:18:02 no 05:19:53 ( Z -- y x 05:19:53 0 : Nat 05:24:05 -!- Slereah_ has joined. 05:25:56 -!- Slereah__ has quit (Ping timeout: 264 seconds). 05:35:45 -!- Bike has joined. 05:38:19 -!- Sellyme has quit (Excess Flood). 05:40:25 -!- Sellyme_ has joined. 05:41:20 -!- Sellyme_ has changed nick to Sellyme. 05:48:52 -!- conehead has joined. 05:49:02 -!- chaiomanot has quit (Quit: Leaving). 06:16:12 -!- trout has quit (Ping timeout: 255 seconds). 07:02:45 -!- ^v has quit (Quit: Leaving). 07:23:59 ( the Type 5 07:23:59 Can't resolve type class Num Type 07:24:05 Worth a shot 07:26:59 was it, sgeo? or have you now violated your most cherished moral principles 07:29:32 Hey, if Int can be a Type 1 and a Type 2 and a Type 3 and ... why shouldn't something lower down be able to participate? 07:30:35 Int can be a Type 2? 07:31:43 ( the (Vect 2 Type) [Int, Type] 07:31:43 [Int, Type] : Vect 2 Type 07:32:09 That Type in the type signature of that has to be Type 1 07:32:22 I think 07:32:36 this seems kind of dumb. 07:36:35 Um, silly question, but if you're on cell 0 in brainfuck, and you do '<', what's the expected behavior? 07:41:54 i think it depends on implementation 07:42:25 sometimes the tape goes infinitely left, sometimes you get an error, sometimes monkeys fly out your nose, that kinda thing? 07:42:34 Good enough. 07:48:27 -!- Bike has quit (Quit: Page closed). 07:50:41 -!- Slereah__ has joined. 07:52:20 -!- Slereah_ has quit (Ping timeout: 264 seconds). 07:53:41 -!- nisstyre_ has quit (Quit: WeeChat 0.4.3). 08:00:24 -!- Slereah_ has joined. 08:02:32 -!- Slereah__ has quit (Ping timeout: 264 seconds). 08:08:50 -!- Slereahphone has joined. 08:11:33 -!- nisstyre has quit (Quit: WeeChat 0.4.3). 08:13:35 -!- Slereahphone has quit (Ping timeout: 252 seconds). 08:27:50 -!- Slereahphone has joined. 08:30:57 -!- Tritonio has joined. 08:47:31 -!- conehead has quit (Quit: Computer has gone to sleep.). 08:48:14 -!- Tritonio has quit (Ping timeout: 252 seconds). 08:51:02 -!- Slereahphone_ has joined. 08:51:36 ( :t 'Foo 08:51:38 'Foo : Type 08:52:05 -!- Slereahphone has quit (Ping timeout: 252 seconds). 08:52:07 -!- Slereahphone_ has changed nick to Slereahphone. 08:52:07 -!- Slereahphone has quit (Client Quit). 09:00:54 -!- mysanthrop has changed nick to myname. 09:04:28 -!- nisstyre has joined. 09:09:43 ( :t Eff 09:09:44 No such variable Eff 09:09:45 aww 09:10:04 Melvar: Should I assume effects will always be a no-go for idris-ircslave? 09:12:43 Yay, I'm "Talkative" on StackOverflow 09:18:23 (I hope that at least requires a space after the paren.) 09:18:28 (Guess so.) 09:19:19 ( the ((a : Type) -> a -> a) the 09:19:20 the : (a : Type) -> a -> a 09:19:29 ( :t o 09:19:29 No such variable o 09:19:33 ( :t (.) 09:19:33 Prelude.Basics.. : (b -> c) -> (a -> b) -> a -> c 09:19:33 Control.Category.. : Category cat => (cat b c) -> (cat a b) -> cat a c 09:20:04 What's a simple dependently typed function that might fail with . 09:21:45 9:15 is the worst time to wake up for an 8:55 train 09:22:20 ( (the . id) Nat 5 09:22:21 (input):1:12:No such variable a 09:22:47 ( (id . the) Nat 5 09:22:48 (input):1:12:No such variable a 09:22:52 :t id . the 09:22:54 Not in scope: `the' 09:22:56 -!- Slereahphone has joined. 09:22:58 ( :t id . the 09:22:59 (input):0:0:No such variable a 09:23:05 ( :t (id .) 09:23:05 Can't disambiguate name: Prelude.Basics.., Control.Category.. 09:23:13 ( :t (id Prelude.Basics.) 09:23:13 (input):1:8:No such variable Prelude.Basics. 09:23:14 -!- Slereah__ has joined. 09:23:19 ( :t (id Prelude.Basics..) 09:23:19 (input):1:8:No such variable Prelude.Basics.. 09:23:26 ( :t (id (Prelude.Basics..)) 09:23:27 (input):1:9:No such variable Prelude.Basics.. 09:23:29 :/ 09:24:57 You and me both 09:24:58 ))))))))))))))))))))))))))))))))))))))))))))))))))) calculated to balance things for this month, so far. 09:25:19 ) 1 2 3 + 4 5 6 09:25:20 Sgeo: 5 7 9 09:25:38 -!- Slereah_ has quit (Ping timeout: 252 seconds). 09:28:58 Actually, based on my current set of logs starting from 2009-03, we actually need 19291 extra opening parens, and my "balancing" just made the total situation worse. 09:29:12 Wonder where all those closing parens come from; there hasn't been *that* much jconn use. 09:29:24 how many come from fungot? 09:29:24 olsner: " i want as much as i loathe how you've manipulated my friends and i are a bit, and if the good. or any room with. simple math dictates the futility of your effort, i have made, it will now go and i will give you my motives and they were not to your liking, would i be carrying our monthly" says that's what my dad, and my time that you are under the empire that has been so deeply disappoi-- 09:31:51 olsner: ...actually it's almost all from ":)" and the like... 09:32:16 hmm, that makes sense 09:32:44 time to start writing (: 09:34:34 Or just be :( all the time. 09:35:32 19291 palindromic parentheses 09:48:27 fizzie: :) 09:48:30 oh 09:48:36 i guess that was answered. 10:01:22 -!- shikhout has joined. 10:02:46 -!- mr45 has joined. 10:03:48 -!- shikhin has quit (Ping timeout: 255 seconds). 10:03:50 -!- shikhout has changed nick to shikhin. 10:07:19 -!- mr45 has left. 10:22:26 -!- nisstyre has quit (Quit: WeeChat 0.4.3). 10:47:03 -!- nooodl has joined. 10:58:35 -!- Slereah__ has quit (Ping timeout: 252 seconds). 11:00:46 -!- Slereah_ has joined. 11:01:41 -!- ggherdov_ has quit (Changing host). 11:01:42 -!- ggherdov_ has joined. 11:01:42 -!- ggherdov_ has quit (Changing host). 11:01:42 -!- ggherdov_ has joined. 11:02:20 -!- ggherdov_ has changed nick to ggherdov. 11:03:05 -!- nooodl has quit (Ping timeout: 252 seconds). 11:12:42 -!- sebbu2 has changed nick to sebbu. 11:35:53 -!- nortti_ has changed nick to nortti. 11:43:12 -!- password2 has joined. 12:03:57 Sgeo, Taneb: It’s “Namespace.(*~)”, the pretty-printer is just still buggy on that bit. 12:06:47 -!- boily has joined. 12:19:19 ( :t the 12:19:19 Prelude.Basics.the : (a : Type) -> a -> a 12:31:51 ( :t the larch 12:31:51 (input):1:8:No such variable larch 12:37:21 > 3+3 12:37:21 6 : Integer 12:37:22 6 12:37:34 idris-ircslave should be configured to not accept > outside of #idris 12:39:59 -!- Sorella has joined. 12:45:54 It doesn’t have any configuration. At all. 12:46:04 ( the Integer 3 12:46:04 3 : Integer 12:47:00 ( the (Fin 5) 3 12:47:00 fS (fS (fS fZ)) : Fin 5 12:47:01 -!- yorick has joined. 12:57:08 ( the (Fin 10) 3 12:57:08 fS (fS (fS fZ)) : Fin 10 12:57:21 ( the (Fin 0) 1 12:57:21 Can't unify 12:57:21 IsJust (Just x) 12:57:21 with 12:57:21 IsJust (integerToFin 1 (fromInteger 0)) 12:57:21 Specifically:↵… 13:22:25 -!- password2 has quit (Ping timeout: 240 seconds). 13:27:50 -!- oerjan has joined. 13:29:47 Hallo oerjan 13:30:04 Ave Taneb 13:30:16 Jafetque 13:32:08 TIL Nethack, Dungeon Crawl and others are based on octagonal tiles in a hyperbolic space. https://github.com/mhwombat/grid/wiki/Octagonal-tiles 13:33:01 wat 13:33:57 fizzie: I sort of think the wiki should have full specs when possible 13:34:01 for archive purposes 13:35:17 I agree 13:37:14 ion: um i am quite suspicious that the connection graphs are the same. 13:37:49 ion: still can't beat the projective 3D goban 13:37:52 like because hyperbolic tilings usually grow exponentially by level, iirc 13:40:54 Well, they become the same if you merge a few to save space (Haskell is after all very bad with memory and we should help it out whenever possible) 13:41:10 OKAY 13:43:19 yep, not the same as https://en.wikipedia.org/wiki/File:Uniform_tiling_83-t0.png 13:43:54 If you place a shape, such as a circle or a square, around (0,0) in https://raw.github.com/mhwombat/grid/master/userguide/images/UnboundedOctGrid.png and start growing the shape, the number of tiles its boundaries touch grows more or less like hyperbolic space, no? 13:44:14 while a cell has 8 neigbors by both countings, those 9 cells have 16 other neighbors in total with the diagonal stuff, but 32 in the hyperbolic one. 13:45:28 which i think is a "no" to your question. 13:46:11 ok 13:46:33 basically, the moore neighborhood "disks" grow linearly sized boundaries, not exponential 13:48:51 http://programmers.stackexchange.com/questions/81624/how-do-computers-work 13:49:21 in fact that hyperbolic picture gets a little hard to read at the next step, but i _think_ it quadruples every new distance. 13:50:00 well logically it should, since it's uniform. 13:50:40 "Another distinctive property is the amount of space covered by the n-ball in hyperbolic n-space: it increases exponentially with respect to the radius of the ball, rather than polynomially." 13:51:16 Jafet: don't post that kind of link after a reading binge of creepy and horror stories. I am now scared post-shitless. 13:51:21 oh hm wait that's not true, some of them have only 3. 13:52:10 boily: http://stackoverflow.com/a/1732454 13:52:18 -!- variable has joined. 13:52:54 Jafet: ah, a classic! I always keep a copy of that one on every machine I own :D 13:53:08 (reminds me to copy it to my newest acquisition) 13:53:24 The text near the end is actually an amazing test for font rendering 13:53:58 -!- Sgeo_ has joined. 13:55:18 oerjan: the border of the image is so tattered that it puts the accuracy of the diagram into question 13:55:31 i suppose 13:57:05 but i think it's actually meant to be varying for two types of octagons at distance 2, according to whether they themselves bound 1 or 2 at distance 1. 13:57:58 -!- Sgeo has quit (Ping timeout: 265 seconds). 13:58:04 TIL: it's en:octagon, but fr:octogon. 13:58:08 the former have 3 exclusive neigbors and 2 more shared on each side, the latter have 2 and 2. 13:58:14 s/n\./ne./ 14:04:51 -!- Slereah_ has quit (Remote host closed the connection). 14:05:05 hm apparently it's oktogon in norwegian. 14:05:12 -!- Slereah_ has joined. 14:06:52 hu 14:07:52 Du latin octogonos, lui-même issu du grec ancien ὀκτώ, oktô (« huit ») et γωνία, gônia (« angle »). 14:08:12 i suspect the latins latinized the vowel a bit. 14:08:42 First attested in 1656, from Latin octagonos, from Ancient Greek οκτάγωνος (oktágōnos, “eight-angled”), from ὀκτώ (octō, “eight”) + γωνία (gōnía, “angle”). 14:09:00 sometimes. 14:09:26 ça fait du sens. 14:09:49 otoh it's latin "octave" 14:09:58 which is pure latin afaik. 14:10:45 (given that it's the common ordinal) 14:12:03 -!- Slereah_ has quit (Remote host closed the connection). 14:12:14 -!- shikhin has quit (Read error: No route to host). 14:12:51 -!- shikhin has joined. 14:12:52 -!- Slereah_ has joined. 14:14:09 but then latin has "octō". 14:14:12 Latin+ ūnus duo trēs quattuor quinque sex septem octō novem decem 14:14:14 Greek éna đío tría téssera pénde éksi eftá oxtó ennéa đéka 14:14:49 that's modern greek, the ancient pronunciation was different see table in https://en.wiktionary.org/wiki/%E1%BD%80%CE%BA%CF%84%CF%8E 14:15:13 -!- variable has quit (Ping timeout: 240 seconds). 14:16:18 also http://www.youtube.com/watch?v=YCFXGanTx4A 14:19:50 -!- password2 has joined. 14:20:21 `relcome password2 14:20:35 ^welcome password2 14:20:35 password2: 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 esote ... 14:20:35 Gregor: IEUAAAAAAAAAAAAAAAAAAARGH! I SHALL MAPOLE YOU! 14:20:47 fungot: stop being so brief 14:20:47 oerjan: of, for-- what does that do? the guild" only worked because belkar and i are a bit, and if my whole life was just leading to one big anticlimax? 14:21:12 oerjan: but that clip only has one two three four. what about the Pronunciation of Eight? 14:21:29 (btw, nice fungotrick.) 14:21:29 boily: good, good. my partner and i were to be connected to anything especialy scandalous. tell him that i said this is where that king guy is as you say that, i thought that the surname came first in feudal deal there and get started, just put my " thank my lord only gave you the really bad, belkar 14:21:40 boily: i am pretty sure at one point in the movie she shouts "oktogonta!" 14:21:58 (when haggling over their rent) 14:22:35 or possibly oxtogonta. 14:23:33 I need to spend more time watching old movies. 14:24:43 well it's been a while since i saw it. 14:24:51 -!- tromp has joined. 14:26:34 trhellomp. 14:26:38 -!- HackEgo has joined. 14:26:49 Gregor: thanks! 14:27:04 `thanks Gregor 14:27:06 No output. 14:27:12 `thank Gregor 14:27:12 No output. 14:27:14 ... 14:27:36 `? canada 14:27:36 No output. 14:28:21 * oerjan suspects foul 14:28:34 oerjan: ‘x’ indicating what there? 14:28:39 oh, so tesseract means four-something, finally makes sense 14:29:15 Melvar: the ipa sound, i guess? 14:29:49 ` 14:29:49 No output. 14:29:55 ``` 14:29:56 No output. 14:30:09 I think a little mapoling is in order at this point. 14:30:11 `you're not really HackEgo are you. since when do you join from an unnamed ip. 14:30:12 No output. 14:30:39 * boily artfully, tesseratically swings his mapole over at Gracenotes 14:30:44 Okay. Just checking, ‘χ’ versus ‘ξ’ and stuff. 14:30:47 s/Gracenotes/Gregor/ 14:31:05 oh hai 14:31:13 Melvar: see the historical pronunciations at https://en.wiktionary.org/wiki/%E1%BD%80%CE%BA%CF%84%CF%8E 14:32:04 Yeah, I'm not really sure what's goin' on right now... 14:32:54 Ohhuh. /x/ from ‹κ›, hadn’t heard of that change. 14:33:10 Gregor: is that actually your bot or is it just someone else faking 14:33:14 password2: so, what brings you over to #esoteric by this fine Saturday morning? 14:33:20 It's my bot. 14:33:23 But it's muy broken. 14:33:24 oops 14:33:57 fungot: with your sentience, can you achieve a HackEgo Impersonation? 14:33:57 boily: i know, i was, uh, any reason... there's no one here but us? we just dueled, he had a name, in accordance with your orders when he instructed the orcs and told me 14:34:06 the repository looks ok 14:34:13 Yeah, it's not that. 14:34:55 -!- HackEgo has quit (Remote host closed the connection). 14:35:10 the problem seems to be that everything gives "No output." instead of e.g. an error 14:35:28 `fnordly go 14:35:34 oh it already went 14:49:41 @r 14:49:41 Maybe you meant: rc reconnect remember repoint roll run v @ ? . 14:49:45 @ru 14:49:46 not an expression: `' 14:51:46 well boily , i have joined this channel a while ago 14:52:12 password2: ah? >_>'... 14:56:39 :) 14:57:23 ( :t Fin 14:57:23 Prelude.Fin.Fin : Nat -> Type 14:57:47 what is that? it looks vaguely haskelly but not quite 14:58:21 "idris" hth 15:02:33 -!- Slereahphone has quit (Quit: Colloquy for iPhone - http://colloquy.mobi). 15:03:00 -!- Slereahphone has joined. 15:09:13 -!- password2 has quit (Ping timeout: 240 seconds). 15:10:00 ( :doc Fin 15:10:00 Data type Fin : Nat -> Type 15:10:00 Numbers strictly less than some bound. The name comes from "finite sets" 15:10:00 Arguments: 15:10:00 n : Nat -- the upper bound 15:10:00 Constructors:↵… 15:14:16 -!- Vorpal has joined. 15:14:22 (Thus, Fin n is inhabited by exactly n values.) 15:15:24 ah, so that's why (Fin 0) 1 doesn't work. 15:16:05 Fin 0 is uninhabited. 15:16:48 ( the (Fin 1) 0 15:16:48 fZ : Fin 1 15:17:22 ( the (Fin 1) 1 15:17:22 Can't unify 15:17:22 IsJust (Just x) 15:17:22 with 15:17:22 IsJust (integerToFin 1 (fromInteger 1)) 15:17:22 Specifically:↵… 15:17:58 I hope the bit of error reflection that turns that into a more digestible message is merged soon. 15:41:03 -!- HackEgo has joined. 15:44:18 -!- impomatic has quit (Ping timeout: 240 seconds). 15:48:13 `echo hi 15:48:19 No output. 15:48:24 Gregor: *cough* 15:53:14 time to phở. 16:01:32 -!- shikhout has joined. 16:04:43 -!- shikhin has quit (Ping timeout: 264 seconds). 16:04:44 -!- shikhout has changed nick to shikhin. 16:08:28 ) :t zipWith 16:08:29 oerjan: |syntax error 16:08:29 oerjan: | :t zipWith 16:08:34 ( :t zipWith 16:08:35 Prelude.List.zipWith : (a -> b -> c) -> (l : List a) -> (r : List b) -> (length l = length r) -> List c 16:08:35 Prelude.Stream.zipWith : (a -> b -> c) -> (Stream a) -> (Stream b) -> Stream c 16:08:35 Prelude.Vect.zipWith : (a -> b -> c) -> (Vect n a) -> (Vect n b) -> Vect n c 16:10:07 ( let fib = 1 :: 1 :: zipWith (+) fib (tail fib) in fib 16:10:09 Can't disambiguate name: Data.HVect.::, Prelude.List.::, Data.Vect.Quantifiers.::, Prelude.Stream.::, Prelude.Vect.:: 16:10:36 ( let fib = the (Stream Integer) (1 :: 1 :: zipWith (+) fib (tail fib)) in fib 16:10:36 Can't unify 16:10:37 Vect n c 16:10:37 with 16:10:37 Stream Integer 16:10:37 Specifically:↵… 16:10:46 hm... 16:10:50 ( :t (::) 16:10:50 Data.HVect.:: : t -> (HVect ts) -> HVect (t :: ts) 16:10:51 Prelude.List.:: : a -> (List a) -> List a 16:10:51 Data.Vect.Quantifiers.:: : (P x) -> (All P xs) -> All P (x :: xs) 16:10:51 Prelude.Stream.:: : a -> (Lazy (Stream a)) -> Stream a 16:10:51 Prelude.Vect.:: : a -> (Vect n a) -> Vect (S n) a 16:11:11 -!- ^v has joined. 16:11:13 ( :t Lazy 16:11:13 Lazy : Type -> Type 16:11:48 ( let fib = the (Lazy (Stream Integer)) (1 :: 1 :: zipWith (+) fib (tail fib)) in fib 16:11:48 Can't unify 16:11:48 Vect n c 16:11:48 with 16:11:48 Stream Integer 16:11:48 Specifically:↵… 16:12:07 this type inference isn't very reliable. 16:12:37 ( let fib : Lazy (Stream Integer); fib = 1 :: 1 :: zipWith (+) fib (tail fib) in fib 16:12:37 (input):1:9: error: expected: "=" 16:12:38 let fib : Lazy (Stream Integer); fib = 1 :: 1 :: zipWith (+) fib (tail fib) in> 16:12:38 ^ 16:13:04 ...you cannot use : in let? 16:13:39 ( :doc Stream 16:13:40 Data type Stream : Type -> Type 16:13:40 An infinite stream 16:13:40 Arguments: 16:13:40 __pi_arg : Type 16:13:40 Constructors:↵… 16:13:59 ( :doc Lazy 16:14:00 Data type Lazy : Type -> Type 16:14:00 Arguments: 16:14:00 __pi_arg : Type 16:14:00 Constructors: 16:14:00 Delay : a -> Lazy a↵… 16:14:04 hm... 16:14:33 ( let fib = Delay (1 :: 1 :: zipWith (+) fib (tail fib)) in fib 16:14:33 Can't disambiguate name: Data.HVect.::, Prelude.List.::, Data.Vect.Quantifiers.::, Prelude.Stream.::, Prelude.Vect.:: 16:15:17 ( let fib = Delay (the (Stream Integer) (1 :: 1 :: zipWith (+) fib (tail fib))) in fib 16:15:17 Can't unify 16:15:18 Vect n c 16:15:18 with 16:15:18 Stream Integer 16:15:18 Specifically:↵… 16:16:15 ( let fib = Delay (1 :: 1 :: Prelude.Stream.zipWith (+) fib (tail fib))) in fib 16:16:16 (input):1:70: error: expected: "$", 16:16:16 "$>", "&&", "&&&", "*", "***", 16:16:16 "+", "++", "-", "->", ".", "/", 16:16:16 "/=", ":+", "::", "<", "<$", 16:16:16 "<$>", "<*>", "<+>", "<->",↵… 16:16:31 ( let fib = Delay (1 :: 1 :: Prelude.Stream.zipWith (+) fib (tail fib)) in fib 16:16:31 Can't unify 16:16:31 Nat -> Nat 16:16:31 with 16:16:31 Stream Nat 16:16:31 Specifically:↵… 16:18:22 ( let fib = Delay (1 Prelude.Stream.:: 1 Prelude.Stream.:: Prelude.Stream.zipWith (+) fib (tail fib)) in fib 16:18:22 (input):1:20:No such variable Prelude.Stream. 16:18:47 ( let fib = Delay (1 Prelude.Stream.(::) 1 Prelude.Stream.(::) Prelude.Stream.zipWith (+) fib (tail fib)) in fib 16:18:47 (input):1:20:Can't infer type for (|(|fromInteger 1 , fromInteger 1 , |) , 1 , 1 , 1 , 1 , 1 , 1 , |) (::) 16:19:10 ( let fib = Delay ((the Integer 1) Prelude.Stream.(::) 1 Prelude.Stream.(::) Prelude.Stream.zipWith (+) fib (tail fib)) in fib 16:19:10 (input):1:34:the Integer (fromInteger 1) does not have a function type (Integer) 16:19:37 ( :t tail 16:19:39 Prelude.List.tail : (l : List a) -> (isCons l = True) -> List a 16:19:39 Prelude.Stream.tail : (Stream a) -> Stream a 16:19:39 Prelude.Vect.tail : (Vect (S n) a) -> Vect n a 16:20:40