00:40:36 <esolangs> [[Parrot]] M https://esolangs.org/w/index.php?diff=119816&oldid=117877 * CreeperBomb * (+18)
02:14:41 -!- zzo38 has quit (Ping timeout: 256 seconds).
03:24:46 -!- ais523 has quit (Ping timeout: 255 seconds).
03:31:31 -!- ais523 has joined.
04:55:14 -!- zzo38 has joined.
05:28:47 -!- Sgeo has quit (Read error: Connection reset by peer).
06:26:13 -!- Sgeo has joined.
06:58:19 -!- ais523 has quit (Quit: quit).
07:18:21 <esolangs> [[Special:Log/move]] move_redir * PythonshellDebugwindow * moved [[Language of Lauging]] to [[Language of Laughing]] over redirect: Fix typo
07:18:21 <esolangs> [[Special:Log/delete]] delete_redir * PythonshellDebugwindow * PythonshellDebugwindow deleted redirect [[Language of Laughing]] by overwriting: Deleted to make way for move from "[[Language of Lauging]]"
07:20:35 <esolangs> [[Language of Laughing]] M https://esolangs.org/w/index.php?diff=119819&oldid=119817 * PythonshellDebugwindow * (+22) Category
07:31:40 -!- tromp has joined.
08:42:05 -!- cpressey has joined.
08:51:22 -!- cpressey has quit (Ping timeout: 250 seconds).
08:55:25 -!- Koen has joined.
09:26:50 -!- cpressey has joined.
09:34:58 -!- __monty__ has joined.
10:03:52 <esolangs> [[Unmatched (]] https://esolangs.org/w/index.php?diff=119820&oldid=119429 * None1 * (+27) /* Python interpreter */ Belongs to the stupid family because of its stupid error reporting feature
10:08:38 <cpressey> "Forward and backward proof in HOL corresponds to special cases of rule composition in Isabelle. However, Milner’s key idea of using ML’s abstract types to ensure that theorems can only be obtained by allowable combinations of allowable rules is retained, and lifted to the metalogic level."
10:09:01 -!- Lord_of_Life has quit (Ping timeout: 276 seconds).
10:09:11 <cpressey> OK, now I'm going to have to look into Isabelle's innards to find out what the heck *that* means.
10:09:25 -!- Lord_of_Life has joined.
10:29:43 <cpressey> Apparently it means the metalogic is implemented as an abstract data type in ML. The object logic that you actually work with, e.g. Isabelle/HOL, is encoded in the metalogic.
10:31:19 <cpressey> That seems less cool somehow. Ah well
11:04:31 -!- Sgeo has quit (Read error: Connection reset by peer).
11:42:59 -!- cpressey has quit (Quit: Client closed).
11:46:07 -!- cpressey has joined.
12:01:41 -!- Koen has quit (Remote host closed the connection).
12:13:42 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
12:14:07 -!- cpressey has quit (Quit: Client closed).
12:16:56 -!- cpressey has joined.
12:19:47 -!- tromp has joined.
13:11:21 -!- Koen has joined.
14:00:46 -!- cpressey has quit (Ping timeout: 250 seconds).
14:10:24 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
14:11:00 -!- cpressey has joined.
14:16:22 -!- tromp has joined.
14:48:06 <esolangs> [[Wiwa]] https://esolangs.org/w/index.php?diff=119821&oldid=119811 * 0ptr * (+56)
15:37:16 <esolangs> [[Kak]] https://esolangs.org/w/index.php?diff=119822&oldid=105501 * ChuckEsoteric08 * (-9)
15:56:14 -!- cpressey has quit (Quit: Client closed).
16:15:46 -!- cpressey has joined.
16:25:37 <riv> I think if you are trying to prove A |- Z (You hvae the assumption A and want to prove B)
16:25:49 <riv> a forward proof step would be using A -> B to change your goal to proving B |- Z
16:26:07 <riv> and a backward proof step would be using Y -> Z to change your goal into A |- Y
16:40:50 -!- Gustof3 has joined.
16:40:51 -!- Koen has quit (Remote host closed the connection).
17:07:24 -!- Gustof3 has quit (Quit: Leaving).
17:25:44 -!- cpressey has quit (Ping timeout: 250 seconds).
17:37:52 <esolangs> [[Monkeys]] M https://esolangs.org/w/index.php?diff=119823&oldid=94835 * PythonshellDebugwindow * (+25) Category
17:53:45 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
18:09:54 -!- tromp has joined.
18:30:55 <esolangs> [[Kak]] https://esolangs.org/w/index.php?diff=119824&oldid=119822 * Quito0567 * (+37) Must be turing complete
18:31:55 <esolangs> [[Kak]] https://esolangs.org/w/index.php?diff=119825&oldid=119824 * Quito0567 * (-37) Undo revision 119824 by [[Special:Contributions/Quito0567|Quito0567]] ([[User talk:Quito0567|talk]]) i take that back
18:38:55 -!- Thelie has joined.
18:39:05 -!- Koen has joined.
19:07:26 -!- esolangs has quit (Ping timeout: 245 seconds).
19:08:05 -!- esolangs1 has joined.
19:08:05 -!- ChanServ has set channel mode: +v esolangs1.
19:09:59 -!- esolangs1 has changed nick to esolangs.
19:31:27 <b_jonas> fungot, are cosmic rays actually cartridge fish, or are they just named after some superficial similarity?
19:31:56 <b_jonas> hmm, our mascot isn't here
19:38:30 <fizzie> Oh²: I updated it to expect the ~ in my hostname when I had that identd issue, which is now resolved (at least temporarily, after a Debian upgrade and reboot), so now it again doesn't acknowledge my authority in commanding it to join here.
19:39:41 -!- fungot has joined.
19:39:51 <fungot> Available: agora alice c64 ct darwin discworld elon enron europarl ff7 fisher fungot homestuck ic irc* iwcs jargon lovecraft nethack oots pa qwantz sms speeches ss wp ukparl youtube
19:40:41 -!- SGautam has joined.
19:54:05 -!- Thelie has quit (Remote host closed the connection).
20:08:58 <b_jonas> fungot, are cosmic rays actually cartridge fish, or are they just named after some superficial similarity?
20:08:58 <fungot> b_jonas: nothing new? spill it) and it is slower then not creating it :)
20:22:00 -!- Sgeo has joined.
20:26:42 <b_jonas> fungot, out of these creatures, which two are what the second word of their name indicates? sea anemone, sea angel, sea ape, sea asparagus, sea bear, sea canary, sea cucumber, sea devil, sea elephant, sea fig, sea hare, sea hawk, sea horse, sea leopard, sea lettuce, sea lilies, sea lion, sea louse, sea moth, sea otter, sea porcupine, sea pork, sea raven, sea toad, sea unicorn, sea urchin, sea vomit, sea
20:26:43 <fungot> b_jonas: i'm looking at gauche to teach myself lots of capsaicin today.
20:30:19 <int-e> "teach myself lots of capsaicin" sounds hot
20:30:26 <int-e> (not in a sexual way)
20:31:31 <fizzie> Possibly relates to sea chilli peppers somehow.
20:32:46 <b_jonas> nah, statistically speaking based on these creatures, sea chili peppers have nothing to do with chili peppers and don't contain capsaicin
20:34:33 <b_jonas> admittedly I was a bit biased when I made that list, I took every name with the referent unrelated to the referent of the second word that I could find, even obsolete names that nobody uses anymore, while I took only two of the twenty or so examples where "sea" is a restricting suffix
20:37:09 <b_jonas> what complicates the matter is that "pepper" is already used for two entirely different groups of plants, one from each side of the ocean
20:59:30 -!- ais523 has joined.
21:07:02 -!- ais523 has quit (Quit: quit).
22:14:08 <tromp> possibly of interest to ppl here: updated version of earlier article at https://tromp.github.io/blog/2023/11/24/largest-number
22:22:54 -!- Koen has quit (Quit: Leaving...).
22:28:17 <esolangs> [[Lazy Prefix]] M https://esolangs.org/w/index.php?diff=119826&oldid=34324 * PythonshellDebugwindow * (+31) Category
22:35:25 <esolangs> [[User:0ptr]] M https://esolangs.org/w/index.php?diff=119827&oldid=119641 * None1 * (-117) It is recommended to use interal links rather than external links for in-esolang links.
22:37:19 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
22:53:53 <esolangs> [[Numeric Batch]] M https://esolangs.org/w/index.php?diff=119828&oldid=75777 * PythonshellDebugwindow * (+63) See also, category
22:59:22 <esolangs> [[MaybeNumericBatch]] M https://esolangs.org/w/index.php?diff=119829&oldid=39054 * PythonshellDebugwindow * (+92) Stub, link, categories
22:59:39 <esolangs> [[MaybeNumericBatch]] M https://esolangs.org/w/index.php?diff=119830&oldid=119829 * PythonshellDebugwindow * (+14) Fix link
23:08:46 -!- ais523 has joined.
23:15:03 -!- SoniEx2 has changed nick to Soni.
23:18:10 -!- ais523 has quit (Quit: sorry about my connection).
23:18:23 -!- ais523 has joined.
23:20:02 -!- SGautam has quit (Quit: Connection closed for inactivity).
23:39:37 -!- __monty__ has quit (Quit: leaving).