| 2024-07-16 00:04:11 +0000 | gabriel_sevecek | (~gabriel@188-167-229-200.dynamic.chello.sk) (Ping timeout: 264 seconds) |
| 2024-07-16 00:04:50 +0000 | Maxdamantus | (~Maxdamant@user/maxdamantus) (Ping timeout: 252 seconds) |
| 2024-07-16 00:05:41 +0000 | gabriel_sevecek | (~gabriel@188-167-229-200.dynamic.chello.sk) |
| 2024-07-16 00:08:11 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 2024-07-16 00:09:45 +0000 | Maxdamantus | (~Maxdamant@user/maxdamantus) |
| 2024-07-16 00:28:58 +0000 | ystael_ | (~ystael@user/ystael) (Ping timeout: 265 seconds) |
| 2024-07-16 00:55:07 +0000 | yin | (~yin@user/zero) (Ping timeout: 268 seconds) |
| 2024-07-16 00:58:59 +0000 | ystael | (~ystael@user/ystael) |
| 2024-07-16 01:00:57 +0000 | tomku | (~tomku@user/tomku) (Ping timeout: 246 seconds) |
| 2024-07-16 01:01:44 +0000 | yin | (~yin@user/zero) |
| 2024-07-16 01:03:06 +0000 | tomku | (~tomku@user/tomku) |
| 2024-07-16 01:06:55 +0000 | ystael | (~ystael@user/ystael) (Ping timeout: 258 seconds) |
| 2024-07-16 01:17:23 +0000 | saraband | (~saraband@pool-173-73-24-54.washdc.fios.verizon.net) |
| 2024-07-16 01:20:35 +0000 | saraband | (~saraband@pool-173-73-24-54.washdc.fios.verizon.net) (Client Quit) |
| 2024-07-16 01:21:54 +0000 | tabemann | (~tabemann@2600:1700:7990:24e0:12ef:2120:f770:f8cc) (Remote host closed the connection) |
| 2024-07-16 01:22:21 +0000 | tabemann | (~tabemann@2600:1700:7990:24e0:7233:7c99:3fac:5c8c) |
| 2024-07-16 01:29:58 +0000 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 245 seconds) |
| 2024-07-16 01:32:06 +0000 | acarrico | (~acarrico@dhcp-68-142-57-215.greenmountainaccess.net) (Quit: Leaving.) |
| 2024-07-16 01:35:11 +0000 | dysthesis | (~dysthesis@user/dysthesis) |
| 2024-07-16 01:37:42 +0000 | aforemny | (~aforemny@2001:9e8:6cd2:fc00:1da8:718a:ae87:dc3a) (Ping timeout: 246 seconds) |
| 2024-07-16 01:38:33 +0000 | aforemny | (~aforemny@89.245.22.200) |
| 2024-07-16 01:43:13 +0000 | g00gler | (uid125351@id-125351.uxbridge.irccloud.com) |
| 2024-07-16 01:52:07 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-07-16 01:58:53 +0000 | harveypwca | (~harveypwc@2601:246:d080:b40:1889:d9bf:2dd8:b288) |
| 2024-07-16 02:02:15 +0000 | <dmj`> | there should be a THIH that uses the constraint solving approach |
| 2024-07-16 02:03:27 +0000 | Square2 | (~Square@user/square) |
| 2024-07-16 02:17:23 +0000 | lain` | (lain`@user/lain/x-9874679) (Ping timeout: 252 seconds) |
| 2024-07-16 02:18:59 +0000 | joeyadams | (~joeyadams@2603:6010:5100:2ed:afa:a01:eb90:b007) |
| 2024-07-16 02:20:27 +0000 | lain` | (lain`@user/lain/x-9874679) |
| 2024-07-16 02:24:33 +0000 | td_ | (~td@i53870911.versanet.de) (Ping timeout: 245 seconds) |
| 2024-07-16 02:26:26 +0000 | td_ | (~td@i53870918.versanet.de) |
| 2024-07-16 02:34:03 +0000 | harveypwca | (~harveypwc@2601:246:d080:b40:1889:d9bf:2dd8:b288) (Quit: Leaving) |
| 2024-07-16 02:39:07 +0000 | vizimajac | (~Rodney@97e7368c.skybroadband.com) (Ping timeout: 264 seconds) |
| 2024-07-16 02:45:43 +0000 | yin | (~yin@user/zero) (Ping timeout: 264 seconds) |
| 2024-07-16 02:51:35 +0000 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-07-16 02:57:56 +0000 | dysthesis | (~dysthesis@user/dysthesis) (Ping timeout: 260 seconds) |
| 2024-07-16 03:07:26 +0000 | vizimajac | (~Rodney@90.201.223.82) |
| 2024-07-16 03:14:18 +0000 | aforemny_ | (~aforemny@2001:9e8:6cee:ed00:5f3f:c04b:274:bbf) |
| 2024-07-16 03:15:43 +0000 | aforemny | (~aforemny@89.245.22.200) (Ping timeout: 265 seconds) |
| 2024-07-16 03:25:36 +0000 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2024-07-16 03:45:05 +0000 | joeyadams | (~joeyadams@2603:6010:5100:2ed:afa:a01:eb90:b007) (Quit: Leaving) |
| 2024-07-16 04:02:06 +0000 | g00gler | (uid125351@id-125351.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-07-16 04:04:36 +0000 | CrunchyFlakes | (~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-07-16 04:07:13 +0000 | CrunchyFlakes | (~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de) |
| 2024-07-16 04:12:52 +0000 | mniip | (mniip@libera/staff/mniip) (*.net *.split) |
| 2024-07-16 04:12:52 +0000 | bastelfreak | (bastelfrea@libera/staff/VoxPupuli.bastelfreak) (*.net *.split) |
| 2024-07-16 04:12:59 +0000 | mniip | (mniip@libera/staff/mniip) |
| 2024-07-16 04:13:13 +0000 | bastelfreak | (bastelfrea@libera/staff/VoxPupuli.bastelfreak) |
| 2024-07-16 04:18:25 +0000 | letsgethexy | (~mrdeeds@173.16.247.92) |
| 2024-07-16 04:25:11 +0000 | spider | (spider@tilde.cafe) (Server closed connection) |
| 2024-07-16 04:25:29 +0000 | spider | (spider@tilde.cafe) |
| 2024-07-16 04:30:28 +0000 | letsgethexy | (~mrdeeds@173.16.247.92) (Remote host closed the connection) |
| 2024-07-16 04:46:25 +0000 | emmanuelux_ | (~emmanuelu@user/emmanuelux) |
| 2024-07-16 04:49:08 +0000 | emmanuelux | (~emmanuelu@user/emmanuelux) (Ping timeout: 245 seconds) |
| 2024-07-16 04:53:36 +0000 | CATS | (apic@brezn3.muc.ccc.de) (Server closed connection) |
| 2024-07-16 04:53:47 +0000 | CATS | (apic@brezn3.muc.ccc.de) |
| 2024-07-16 04:55:47 +0000 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2024-07-16 04:56:42 +0000 | int-e | (~noone@int-e.eu) (Server closed connection) |
| 2024-07-16 04:56:52 +0000 | int-e | (~noone@int-e.eu) |
| 2024-07-16 04:57:17 +0000 | aws | (~alews@user/aws) (Server closed connection) |
| 2024-07-16 04:57:34 +0000 | aws | (~alews@user/aws) |
| 2024-07-16 05:13:02 +0000 | tcard | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Remote host closed the connection) |
| 2024-07-16 05:13:15 +0000 | tcard | (~tcard@2400:4051:5801:7500:1e90:74c3:2754:ce8a) |
| 2024-07-16 05:30:21 +0000 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-07-16 05:33:57 +0000 | misterfish | (~misterfis@84.53.85.146) (Ping timeout: 246 seconds) |
| 2024-07-16 05:34:29 +0000 | sweater | (~sweater@206.81.18.26) (Server closed connection) |
| 2024-07-16 05:34:47 +0000 | sweater | (~sweater@206.81.18.26) |
| 2024-07-16 05:38:48 +0000 | acidjnk | (~acidjnk@p200300d6e72cfb805cd63c25806f679d.dip0.t-ipconnect.de) |
| 2024-07-16 05:40:46 +0000 | brettgilio | (~brettgili@154.3.237.18) |
| 2024-07-16 05:43:47 +0000 | ario | (~ario@159.65.220.102) (Server closed connection) |
| 2024-07-16 05:43:55 +0000 | ario | (~ario@159.65.220.102) |
| 2024-07-16 05:44:45 +0000 | byte | (~byte@149.28.222.189) (Server closed connection) |
| 2024-07-16 05:45:03 +0000 | byte | (~byte@149.28.222.189) |
| 2024-07-16 05:48:42 +0000 | glguy | (g@libera/staff/glguy) (Read error: Connection reset by peer) |
| 2024-07-16 05:49:29 +0000 | vgtw | (~vgtw@user/vgtw) |
| 2024-07-16 05:51:33 +0000 | glguy | (glguy@libera/staff/glguy) |
| 2024-07-16 06:01:12 +0000 | rosco | (~rosco@175.136.155.137) |
| 2024-07-16 06:01:39 +0000 | bilegeek | (~bilegeek@2600:1008:b09a:c2ab:ba0b:9828:fe58:2964) |
| 2024-07-16 06:07:06 +0000 | vgtw | (~vgtw@user/vgtw) (Quit: ZNC - https://znc.in) |
| 2024-07-16 06:18:20 +0000 | Dykam | (Dykam@dykam.nl) (Server closed connection) |
| 2024-07-16 06:18:33 +0000 | Dykam | (Dykam@dykam.nl) |
| 2024-07-16 06:20:43 +0000 | ethantwardy | (user@user/ethantwardy) (Ping timeout: 268 seconds) |
| 2024-07-16 06:20:43 +0000 | mmaruseacph2 | (~mihai@mihai.page) (Ping timeout: 268 seconds) |
| 2024-07-16 06:20:58 +0000 | mmaruseacph2 | (~mihai@mihai.page) |
| 2024-07-16 06:21:07 +0000 | ethantwardy | (user@user/ethantwardy) |
| 2024-07-16 06:21:21 +0000 | meejah | (~meejah@104.236.166.239) (Ping timeout: 268 seconds) |
| 2024-07-16 06:22:47 +0000 | meejah | (~meejah@rutas.meejah.ca) |
| 2024-07-16 06:24:12 +0000 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2024-07-16 06:30:44 +0000 | joeyh_ | (~joeyh@kitenet.net) (Server closed connection) |
| 2024-07-16 06:30:55 +0000 | joeyh | (~joeyh@kitenet.net) |
| 2024-07-16 06:32:12 +0000 | m1dnight | (~christoph@82.146.125.185) (Quit: WeeChat 4.2.2) |
| 2024-07-16 06:32:53 +0000 | m1dnight | (~christoph@82.146.125.185) |
| 2024-07-16 06:44:41 +0000 | lockna_ | (~lockna@static.139.16.130.94.clients.your-server.de) (Server closed connection) |
| 2024-07-16 06:44:55 +0000 | lockna | (~lockna@2a01:4f8:10b:14f1::2) |
| 2024-07-16 06:48:09 +0000 | gmg | (~user@user/gehmehgeh) |
| 2024-07-16 06:48:55 +0000 | JimL | (~quassel@89.162.16.26) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 2024-07-16 06:55:36 +0000 | __monty__ | (~toonn@user/toonn) |
| 2024-07-16 06:57:36 +0000 | mima | (~mmh@user/mima) (Server closed connection) |
| 2024-07-16 06:57:51 +0000 | mima | (~mmh@user/mima) |
| 2024-07-16 06:58:23 +0000 | pointlessslippe1 | (~pointless@212.82.82.3) |
| 2024-07-16 07:00:01 +0000 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-07-16 07:00:32 +0000 | xelxebar | (~xelxebar@wilsonb.com) (Quit: ZNC 1.7.2+deb3 - https://znc.in) |
| 2024-07-16 07:02:30 +0000 | Maxdamantus | (~Maxdamant@user/maxdamantus) (Ping timeout: 246 seconds) |
| 2024-07-16 07:04:22 +0000 | Maxdamantus | (~Maxdamant@user/maxdamantus) |
| 2024-07-16 07:06:23 +0000 | tdammers_ | (~tdammers@41-138-178-143.ftth.glasoperator.nl) (Server closed connection) |
| 2024-07-16 07:06:46 +0000 | tdammers_ | (~tdammers@41-138-178-143.ftth.glasoperator.nl) |
| 2024-07-16 07:08:34 +0000 | vgtw | (~vgtw@user/vgtw) |
| 2024-07-16 07:14:31 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 264 seconds) |
| 2024-07-16 07:17:40 +0000 | xelxebar | (~xelxebar@wilsonb.com) |
| 2024-07-16 07:24:36 +0000 | xelxebar | (~xelxebar@wilsonb.com) (Quit: ZNC 1.7.2+deb3 - https://znc.in) |
| 2024-07-16 07:24:48 +0000 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-07-16 07:25:02 +0000 | xelxebar | (~xelxebar@wilsonb.com) |
| 2024-07-16 07:27:02 +0000 | puke | (~puke@user/puke) (Remote host closed the connection) |
| 2024-07-16 07:33:37 +0000 | xelxebar | (~xelxebar@wilsonb.com) (Quit: ZNC 1.7.2+deb3 - https://znc.in) |
| 2024-07-16 07:34:02 +0000 | xelxebar | (~xelxebar@wilsonb.com) |
| 2024-07-16 07:40:29 +0000 | quintasan | (~quassel@quintasan.pl) (Server closed connection) |
| 2024-07-16 07:40:38 +0000 | quintasan | (~quassel@quintasan.pl) |
| 2024-07-16 07:43:25 +0000 | emmanuelux_ | (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 2024-07-16 07:44:21 +0000 | ft | (~ft@p4fc2ab80.dip0.t-ipconnect.de) (Quit: leaving) |
| 2024-07-16 07:52:06 +0000 | euleritian | (~euleritia@pd9ebb103.dip0.t-ipconnect.de) (Ping timeout: 258 seconds) |
| 2024-07-16 07:53:14 +0000 | cpressey | (~weechat@176.254.71.203) |
| 2024-07-16 07:55:23 +0000 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-07-16 07:56:49 +0000 | euleritian | (~euleritia@dynamic-176-005-135-121.176.5.pool.telefonica.de) |
| 2024-07-16 07:57:52 +0000 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-07-16 08:18:12 +0000 | tstat | (~tstat@user/tstat) (Server closed connection) |
| 2024-07-16 08:19:00 +0000 | tstat | (~tstat@user/tstat) |
| 2024-07-16 08:19:11 +0000 | misterfish | (~misterfis@87.215.131.102) |
| 2024-07-16 08:20:38 +0000 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-07-16 08:23:25 +0000 | danse-nr3 | (~danse-nr3@151.37.183.46) |
| 2024-07-16 08:23:52 +0000 | JamesMowery | (~JamesMowe@ip98-167-207-182.ph.ph.cox.net) (Quit: Ping timeout (120 seconds)) |
| 2024-07-16 08:24:12 +0000 | JamesMowery | (~JamesMowe@ip98-167-207-182.ph.ph.cox.net) |
| 2024-07-16 08:32:50 +0000 | danse-nr3 | (~danse-nr3@151.37.183.46) (Ping timeout: 248 seconds) |
| 2024-07-16 08:36:34 +0000 | dolio | (~dolio@130.44.134.54) (Ping timeout: 264 seconds) |
| 2024-07-16 08:37:02 +0000 | danse-nr3 | (~danse-nr3@151.37.183.46) |
| 2024-07-16 08:43:25 +0000 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 2024-07-16 08:45:39 +0000 | CiaoSen | (~Jura@2a05:5800:2b3:5600:e6b9:7aff:fe80:3d03) |
| 2024-07-16 08:46:41 +0000 | bryanv | (~quassel@2603:c028:4503:7500:45b7:933:ab17:bc10) (Server closed connection) |
| 2024-07-16 08:46:55 +0000 | bryanv | (~quassel@2603:c028:4503:7500:45b7:933:ab17:bc10) |
| 2024-07-16 08:52:16 +0000 | dolio | (~dolio@130.44.134.54) |
| 2024-07-16 08:58:17 +0000 | yangby | (~secret@115.204.116.173) |
| 2024-07-16 09:01:38 +0000 | dolio | (~dolio@130.44.134.54) (Ping timeout: 272 seconds) |
| 2024-07-16 09:03:28 +0000 | bilegeek | (~bilegeek@2600:1008:b09a:c2ab:ba0b:9828:fe58:2964) (Quit: Leaving) |
| 2024-07-16 09:17:23 +0000 | JamesMowery0 | (~JamesMowe@ip98-167-207-182.ph.ph.cox.net) |
| 2024-07-16 09:19:14 +0000 | JamesMowery | (~JamesMowe@ip98-167-207-182.ph.ph.cox.net) (Ping timeout: 248 seconds) |
| 2024-07-16 09:19:14 +0000 | JamesMowery0 | JamesMowery |
| 2024-07-16 09:19:48 +0000 | danse-nr3 | (~danse-nr3@151.37.183.46) (Changing host) |
| 2024-07-16 09:19:48 +0000 | danse-nr3 | (~danse-nr3@user/danse-nr3) |
| 2024-07-16 09:26:24 +0000 | abrar | (~abrar@pool-72-78-199-167.phlapa.fios.verizon.net) (Server closed connection) |
| 2024-07-16 09:26:42 +0000 | misterfish | (~misterfis@87.215.131.102) (Ping timeout: 248 seconds) |
| 2024-07-16 09:26:48 +0000 | abrar | (~abrar@pool-72-78-199-167.phlapa.fios.verizon.net) |
| 2024-07-16 09:28:40 +0000 | misterfish | (~misterfis@178.225.158.139) |
| 2024-07-16 09:34:02 +0000 | chele | (~chele@user/chele) |
| 2024-07-16 09:44:29 +0000 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) (Server closed connection) |
| 2024-07-16 09:45:53 +0000 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) |
| 2024-07-16 09:59:59 +0000 | stefan-_ | (~cri@42dots.de) (Server closed connection) |
| 2024-07-16 10:00:14 +0000 | stefan-_ | (~cri@42dots.de) |
| 2024-07-16 10:00:16 +0000 | Jackneill_ | (~Jackneill@178-164-177-183.pool.digikabel.hu) (Quit: Leaving) |
| 2024-07-16 10:10:23 +0000 | enikar | (~enikar@user/enikar) (Server closed connection) |
| 2024-07-16 10:10:42 +0000 | enikar | (~enikar@user/enikar) |
| 2024-07-16 10:11:17 +0000 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2024-07-16 10:21:27 +0000 | <tromp> | what is the type of Church numeral 2 in CoC (Calculus of Constructions) ? Is it Nat = forall(a : *) -> (a -> a) -> a -> a ? |
| 2024-07-16 10:23:08 +0000 | Square2 | (~Square@user/square) (Ping timeout: 258 seconds) |
| 2024-07-16 10:25:14 +0000 | <ncf> | all church numerals have the same type |
| 2024-07-16 10:25:30 +0000 | mikess | (~mikess@user/mikess) (Ping timeout: 246 seconds) |
| 2024-07-16 10:28:02 +0000 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Ping timeout: 248 seconds) |
| 2024-07-16 10:39:00 +0000 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-07-16 10:39:46 +0000 | <tromp> | got disconnected; hope I didn't miss an answer... |
| 2024-07-16 10:40:53 +0000 | <ncf> | all church numerals have the same type |
| 2024-07-16 10:51:56 +0000 | <tromp> | i know |
| 2024-07-16 10:52:17 +0000 | <tromp> | is that the correct type? |
| 2024-07-16 10:52:53 +0000 | <ncf> | sure |
| 2024-07-16 10:53:25 +0000 | <tromp> | is that short for forall(a : *) -> forall(_ : (forall(_ : a -> a)) -> forall(_ : a) -> a ? |
| 2024-07-16 10:54:31 +0000 | <tromp> | i.e. 4 uses of the Pi constructor? |
| 2024-07-16 10:55:49 +0000 | <ncf> | yes |
| 2024-07-16 10:56:40 +0000 | <ncf> | (a : *) → (_ : (_ : a) → a) → (_ : a) → a |
| 2024-07-16 10:59:14 +0000 | <tromp> | Thanks. Does anyone know of a Haskell implementation of Loader's Number? https://googology.fandom.com/wiki/Loader%27s_number |
| 2024-07-16 11:03:16 +0000 | <ncf> | that would be cool, but i don't |
| 2024-07-16 11:10:17 +0000 | mreh | (~matthew@host86-160-168-12.range86-160.btcentralplus.com) |
| 2024-07-16 11:10:19 +0000 | danse-nr3 | (~danse-nr3@user/danse-nr3) (Quit: Leaving) |
| 2024-07-16 11:19:33 +0000 | mcfrdy | (~mcfrdy@user/mcfrdy) (Server closed connection) |
| 2024-07-16 11:19:53 +0000 | mcfrdy | (~mcfrdy@user/mcfrdy) |
| 2024-07-16 11:21:21 +0000 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Ping timeout: 260 seconds) |
| 2024-07-16 11:23:35 +0000 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
| 2024-07-16 11:28:06 +0000 | sprout | (~quassel@2a02-a448-3a80-0-bd3d-b7cf-ad17-1736.fixed6.kpn.net) (Read error: Connection reset by peer) |
| 2024-07-16 11:31:58 +0000 | sprout | (~quassel@2a02-a448-3a80-0-1da5-990b-8c01-534d.fixed6.kpn.net) |
| 2024-07-16 11:36:22 +0000 | misterfish | (~misterfis@178.225.158.139) (Ping timeout: 244 seconds) |
| 2024-07-16 11:37:11 +0000 | emergence | (emergence@2607:5300:60:5910:dcad:beff:feef:5bc) (Server closed connection) |
| 2024-07-16 11:37:23 +0000 | emergence | (emergence@2607:5300:60:5910:dcad:beff:feef:5bc) |
| 2024-07-16 11:37:59 +0000 | misterfish | (~misterfis@87.215.131.102) |
| 2024-07-16 11:41:11 +0000 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Ping timeout: 260 seconds) |
| 2024-07-16 11:41:35 +0000 | yangby | (~secret@115.204.116.173) (Quit: Go out for a walk and buy a drink.) |
| 2024-07-16 11:41:39 +0000 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2024-07-16 11:56:51 +0000 | td_ | (~td@i53870918.versanet.de) (Ping timeout: 246 seconds) |
| 2024-07-16 11:57:04 +0000 | td_ | (~td@i53870918.versanet.de) |
| 2024-07-16 12:01:06 +0000 | nullie | (~nullie@2a01:4f8:c2c:6177::1) (Quit: WeeChat 4.2.2) |
| 2024-07-16 12:01:10 +0000 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-07-16 12:01:24 +0000 | hexeme | (~hexeme@user/hexeme) (Server closed connection) |
| 2024-07-16 12:01:25 +0000 | nullie | (~nullie@2a01:4f8:c2c:6177::1) |
| 2024-07-16 12:02:19 +0000 | hexeme | (~hexeme@user/hexeme) |
| 2024-07-16 12:04:23 +0000 | nullie | (~nullie@2a01:4f8:c2c:6177::1) (Client Quit) |
| 2024-07-16 12:04:40 +0000 | cpressey | (~weechat@176.254.71.203) (Ping timeout: 272 seconds) |
| 2024-07-16 12:04:46 +0000 | nullie | (~nullie@2a01:4f8:c2c:6177::1) |
| 2024-07-16 12:05:40 +0000 | nullie | (~nullie@2a01:4f8:c2c:6177::1) (Client Quit) |
| 2024-07-16 12:05:57 +0000 | nullie | (~nullie@nuremberg.nullie.name) |
| 2024-07-16 12:08:30 +0000 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2024-07-16 12:11:12 +0000 | ddellacosta | (~ddellacos@ool-44c73d29.dyn.optonline.net) (Ping timeout: 246 seconds) |
| 2024-07-16 12:40:33 +0000 | m5zs7k | (aquares@web10.mydevil.net) (Ping timeout: 252 seconds) |
| 2024-07-16 12:40:55 +0000 | AlexZenon | (~alzenon@178.34.160.117) (Quit: ;-) |
| 2024-07-16 12:41:45 +0000 | AlexNoo | (~AlexNoo@178.34.160.117) (Quit: Leaving) |
| 2024-07-16 12:42:33 +0000 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-07-16 12:43:38 +0000 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Client Quit) |
| 2024-07-16 12:45:24 +0000 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-07-16 12:46:21 +0000 | Sciencentistguy | (~sciencent@hacksoc/ordinary-member) (Server closed connection) |
| 2024-07-16 12:46:43 +0000 | Sciencentistguy | (~sciencent@hacksoc/ordinary-member) |
| 2024-07-16 12:49:50 +0000 | yin | (~yin@user/zero) |
| 2024-07-16 12:50:18 +0000 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2024-07-16 12:50:39 +0000 | califax | (~califax@user/califx) |
| 2024-07-16 12:54:06 +0000 | MironZ3 | (~MironZ@nat-infra.ehlab.uk) (Server closed connection) |
| 2024-07-16 12:54:29 +0000 | MironZ3 | (~MironZ@nat-infra.ehlab.uk) |
| 2024-07-16 12:58:21 +0000 | Square2 | (~Square@user/square) |
| 2024-07-16 13:06:53 +0000 | cpressey | (~weechat@176.254.71.203) |
| 2024-07-16 13:07:06 +0000 | <haskellbridge> | <mauke> Why are messages from ncf shown as coming from "haskellbridge" on the Matrix side? |
| 2024-07-16 13:13:55 +0000 | m5zs7k | (aquares@web10.mydevil.net) |
| 2024-07-16 13:16:46 +0000 | AlexNoo | (~AlexNoo@178.34.160.117) |
| 2024-07-16 13:17:10 +0000 | AlexZenon | (~alzenon@178.34.160.117) |
| 2024-07-16 13:17:54 +0000 | <ncf> | um, because i'm on irc? |
| 2024-07-16 13:19:06 +0000 | <ncf> | test |
| 2024-07-16 13:20:20 +0000 | <ncf> | yeah i guess that's weird. geekosaur? |
| 2024-07-16 13:23:26 +0000 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) |
| 2024-07-16 13:31:15 +0000 | <EvanR> | test |
| 2024-07-16 13:50:47 +0000 | hugo- | (hugo@quicksilver.lysator.liu.se) (Quit: ZNC 1.8.2+deb3.1 - https://znc.in) |
| 2024-07-16 14:06:58 +0000 | ystael | (~ystael@user/ystael) |
| 2024-07-16 14:14:42 +0000 | kaol | (~kaol@94-237-42-30.nl-ams1.upcloud.host) (Server closed connection) |
| 2024-07-16 14:14:49 +0000 | kaol | (~kaol@94-237-42-30.nl-ams1.upcloud.host) |
| 2024-07-16 14:15:46 +0000 | chiselfuse | (~chiselfus@user/chiselfuse) (Ping timeout: 260 seconds) |
| 2024-07-16 14:16:51 +0000 | chiselfuse | (~chiselfus@user/chiselfuse) |
| 2024-07-16 14:29:06 +0000 | <geekosaur> | "view raw" says your client is sending notices instead of messages |
| 2024-07-16 14:29:23 +0000 | <geekosaur> | …wait, but it just did that to mine too |
| 2024-07-16 14:30:05 +0000 | haskellbridge | (~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection) |
| 2024-07-16 14:30:25 +0000 | <geekosaur> | uh oh |
| 2024-07-16 14:30:27 +0000 | haskellbridge | (~hackager@syn-024-093-192-219.res.spectrum.com) |
| 2024-07-16 14:30:27 +0000 | ChanServ | +v haskellbridge |
| 2024-07-16 14:31:04 +0000 | <tomsmeding> | test |
| 2024-07-16 14:31:11 +0000 | kritzefitz | (~kritzefit@debian/kritzefitz) (Ping timeout: 264 seconds) |
| 2024-07-16 14:31:21 +0000 | <geekosaur> | foo |
| 2024-07-16 14:31:45 +0000 | <geekosaur> | working now |
| 2024-07-16 14:31:57 +0000 | <ncf> | 🐝 |
| 2024-07-16 14:32:15 +0000 | <mauke> | what happen? |
| 2024-07-16 14:32:23 +0000 | chiselfuse | (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 2024-07-16 14:32:24 +0000 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2024-07-16 14:32:24 +0000 | <geekosaur> | dunno |
| 2024-07-16 14:32:25 +0000 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2024-07-16 14:32:25 +0000 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2024-07-16 14:32:33 +0000 | <ncf> | yay |
| 2024-07-16 14:32:39 +0000 | chexum | (~quassel@gateway/tor-sasl/chexum) |
| 2024-07-16 14:32:57 +0000 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
| 2024-07-16 14:33:10 +0000 | chiselfuse | (~chiselfus@user/chiselfuse) |
| 2024-07-16 14:33:10 +0000 | <geekosaur> | I did restart it a couple days ago, maybe they had a bad update (I'm running from their `latest` docker container) |
| 2024-07-16 14:33:20 +0000 | gmg | (~user@user/gehmehgeh) |
| 2024-07-16 14:40:05 +0000 | deriamis_ | (deriamis@ec2-54-187-167-69.us-west-2.compute.amazonaws.com) (Server closed connection) |
| 2024-07-16 14:41:04 +0000 | deriamis | (deriamis@2600:1f14:1251:ba02:2994:f9dc:75a8:113b) |
| 2024-07-16 14:48:53 +0000 | <haskellbridge> | <thirdofmay18081814goya> anyone got suggestions for declaring nested records to parse a nested json object? any extension that would allow me to declare a single nested record data type instead of needing to make a new data type for each subsequent nested record? |
| 2024-07-16 14:49:18 +0000 | <haskellbridge> | <thirdofmay18081814goya> e.g. i'd like to make a data type that models |
| 2024-07-16 14:49:18 +0000 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_matrix/media/v3/download/kf8nh.com/fJODeknIoqILfAADEYDhRSUD (27 lines) |
| 2024-07-16 14:50:55 +0000 | kritzefitz | (~kritzefit@debian/kritzefitz) |
| 2024-07-16 14:52:11 +0000 | <mauke> | with aeson, wouldn't that just be custom FromJSON/ToJSON instances? |
| 2024-07-16 14:52:33 +0000 | <haskellbridge> | <thirdofmay18081814goya> mauke: yeah but i'd like to declare it in a single data type |
| 2024-07-16 14:52:40 +0000 | <mauke> | except you don't get "nested records" on the haskell side |
| 2024-07-16 14:52:50 +0000 | <mauke> | you can do it with a flat record, though |
| 2024-07-16 14:53:23 +0000 | zetef | (~quassel@82.76.106.80) |
| 2024-07-16 14:53:44 +0000 | zetef | (~quassel@82.76.106.80) (Client Quit) |
| 2024-07-16 14:54:21 +0000 | ash3en | (~ash3en@89.246.174.164) |
| 2024-07-16 14:54:29 +0000 | <haskellbridge> | <thirdofmay18081814goya> mauke: yeah purely as a question of presentation i wanted to avoid multiple flat records |
| 2024-07-16 14:54:47 +0000 | <tomsmeding> | what would the desired set of data types be? |
| 2024-07-16 14:54:56 +0000 | <tomsmeding> | if you don't want nested records |
| 2024-07-16 14:54:59 +0000 | <mauke> | ... multiple? |
| 2024-07-16 14:55:14 +0000 | <tomsmeding> | or is it "I want the normal thing but I want to type less code" |
| 2024-07-16 14:55:50 +0000 | <haskellbridge> | <thirdofmay18081814goya> mauke: yeah, one record for the "response" data type, and another for each nested record within "response": "identity", "stock", "dimensions", etc. |
| 2024-07-16 14:56:53 +0000 | <tomsmeding> | there is no extension that will create that set of data types for you from some smaller description of the structure |
| 2024-07-16 14:57:05 +0000 | <tomsmeding> | you could write some TemplateHaskell and make it though :p |
| 2024-07-16 14:57:16 +0000 | <cheater> | i was just going to say that TH is one such extension |
| 2024-07-16 14:57:46 +0000 | <haskellbridge> | <thirdofmay18081814goya> yeah might be a template haskell question, i have multiple of these i'd like to define. really i just want to have a nice self-contained type declaration i can look at, it's not for any other reason |
| 2024-07-16 14:57:52 +0000 | <haskellbridge> | <thirdofmay18081814goya> will look up how i might do this with TH, ty |
| 2024-07-16 14:58:18 +0000 | <mauke> | https://hackage.haskell.org/package/aeson-2.2.3.0/docs/Data-Aeson.html#g:2 |
| 2024-07-16 14:58:28 +0000 | <cheater> | can it be you're just not used to what haskell looks like |
| 2024-07-16 14:58:43 +0000 | <cheater> | sometimes the best hack is no hack at all |
| 2024-07-16 14:58:56 +0000 | <cheater> | keep doing things the way god intended |
| 2024-07-16 14:59:54 +0000 | ddellacosta | (~ddellacos@ool-44c73d29.dyn.optonline.net) |
| 2024-07-16 15:00:12 +0000 | <haskellbridge> | <thirdofmay18081814goya> heheh it's possible, but i enjoy typescript's self-contained presentation of this sort of type |
| 2024-07-16 15:00:15 +0000 | <ash3en> | what is the TH situation? is this not needed magic hackery causing headaches or superior meta programming for pros? |
| 2024-07-16 15:00:48 +0000 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) |
| 2024-07-16 15:01:05 +0000 | <ash3en> | or rephrased: is TH elegant? |
| 2024-07-16 15:02:19 +0000 | <tomsmeding> | that is in the eye of the beholder :) |
| 2024-07-16 15:02:56 +0000 | <mauke> | yesn't |
| 2024-07-16 15:04:18 +0000 | ddellacosta | (~ddellacos@ool-44c73d29.dyn.optonline.net) (Ping timeout: 248 seconds) |
| 2024-07-16 15:07:07 +0000 | <ash3en> | intuively it *feels* like a liability and breaking haskell concepts. but otoh it may use haskell to it's fullest! arghh help lol |
| 2024-07-16 15:13:00 +0000 | misterfish | (~misterfis@87.215.131.102) (Ping timeout: 252 seconds) |
| 2024-07-16 15:13:54 +0000 | <haskellbridge> | <thirdofmay18081814goya> there's an anonymous records library that's being maintained |
| 2024-07-16 15:13:55 +0000 | <haskellbridge> | <thirdofmay18081814goya> "large-anon" |
| 2024-07-16 15:16:05 +0000 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2024-07-16 15:16:34 +0000 | mreh | (~matthew@host86-160-168-12.range86-160.btcentralplus.com) (Ping timeout: 248 seconds) |
| 2024-07-16 15:19:48 +0000 | kosmikus | (~kosmikus@nullzig.kosmikus.org) (Server closed connection) |
| 2024-07-16 15:20:00 +0000 | kosmikus | (~kosmikus@nullzig.kosmikus.org) |
| 2024-07-16 15:22:52 +0000 | <haskellbridge> | <thirdofmay18081814goya> found someone who already did the work: https://github.com/brandonchinn178/aeson-schemas |
| 2024-07-16 15:23:01 +0000 | <haskellbridge> | <thirdofmay18081814goya> bless 'em |
| 2024-07-16 15:30:41 +0000 | <EvanR> | last resort TH is also bad because of compile times |
| 2024-07-16 15:30:57 +0000 | <tomsmeding> | what is "last resort TH"? |
| 2024-07-16 15:31:40 +0000 | <EvanR> | just TH |
| 2024-07-16 15:32:09 +0000 | <EvanR> | metaprogramming = missing language feature |
| 2024-07-16 15:32:36 +0000 | <tomsmeding> | or experimental language feature |
| 2024-07-16 15:32:55 +0000 | <tomsmeding> | or language feature that would be nice but would unnecessarily burden the maintainers of the language implementation for something that only you use |
| 2024-07-16 15:33:07 +0000 | <tomsmeding> | metaprogramming _is_ a language feature |
| 2024-07-16 15:33:31 +0000 | <tomsmeding> | to the extent that various languages do metaprogramming in vastly different ways |
| 2024-07-16 15:34:19 +0000 | <tomsmeding> | Rust even has two: macro_rules! and procedural macros |
| 2024-07-16 15:35:24 +0000 | <EvanR> | it covers all missing language features |
| 2024-07-16 15:35:45 +0000 | <EvanR> | but not necessarily in the best and most efficient way |
| 2024-07-16 15:35:45 +0000 | <tomsmeding> | no, there are language features that you cannot cover with most existing metaprogramming designs |
| 2024-07-16 15:35:57 +0000 | <EvanR> | like what |
| 2024-07-16 15:36:08 +0000 | <tomsmeding> | IO from a language that doesn't have IO? |
| 2024-07-16 15:36:21 +0000 | <EvanR> | how does this apply to TH |
| 2024-07-16 15:36:28 +0000 | <tomsmeding> | you were talking about metaprogramming in general :p |
| 2024-07-16 15:36:45 +0000 | <EvanR> | yeah there is crippled metaprogramming |
| 2024-07-16 15:36:51 +0000 | <EvanR> | like C preprocessor |
| 2024-07-16 15:37:05 +0000 | <tomsmeding> | no matter how good your metaprogramming, if the base language does not have IO, you're not going to metaprogram yourself to IO |
| 2024-07-16 15:37:19 +0000 | <EvanR> | by IO are you just talking about a type system |
| 2024-07-16 15:37:35 +0000 | <EvanR> | clearly most languages have I/O |
| 2024-07-16 15:37:38 +0000 | <tomsmeding> | no I mean stuff like lua where if the host does not give you IO libraries, you _cannot do IO_ |
| 2024-07-16 15:38:02 +0000 | <tomsmeding> | which is the point of lua as an embedded language, the host can restrict what kind of side effects are possible |
| 2024-07-16 15:38:18 +0000 | <tomsmeding> | by simply not giving you the functions which would perform those side effects |
| 2024-07-16 15:38:21 +0000 | <EvanR> | lua has I/O unless you go out of your way to cripple it and move it to the host |
| 2024-07-16 15:38:32 +0000 | <EvanR> | but I don't know if this matters to the argument |
| 2024-07-16 15:38:46 +0000 | <tomsmeding> | I took issue with your blanket statements that metaprogramming fixes all problems :p |
| 2024-07-16 15:38:53 +0000 | <EvanR> | it doesn't really have metaprogramming |
| 2024-07-16 15:39:18 +0000 | <tomsmeding> | and even assuming that you're in a turing-complete language with side effects etc, you could perhaps theoretically map any kind of code to whatever you want it to mean |
| 2024-07-16 15:39:30 +0000 | <tomsmeding> | but it's not like that's practical or a decent way to implement a missing language feature :p |
| 2024-07-16 15:39:39 +0000 | <EvanR> | that's what I was saying |
| 2024-07-16 15:39:52 +0000 | <tomsmeding> | then why do you say "it covers all missing language features" |
| 2024-07-16 15:39:57 +0000 | <tomsmeding> | technically correct, maybe |
| 2024-07-16 15:40:27 +0000 | <tomsmeding> | still, I could want interactive hole filling in haskell |
| 2024-07-16 15:40:28 +0000 | <EvanR> | stop argeeing! |
| 2024-07-16 15:40:32 +0000 | <tomsmeding> | is that a language feature or a compiler feature? |
| 2024-07-16 15:40:39 +0000 | <tomsmeding> | lol |
| 2024-07-16 15:40:59 +0000 | <tomsmeding> | as in, "technically correct if you choose unhelpful definitions of the words in question" |
| 2024-07-16 15:41:13 +0000 | <tomsmeding> | anyway this discussion got longer than it was meant to lol |
| 2024-07-16 15:41:36 +0000 | <tomsmeding> | sorry for the rant |
| 2024-07-16 15:42:07 +0000 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2024-07-16 15:42:18 +0000 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) (ERC (IRC client for Emacs 27.1)) |
| 2024-07-16 15:42:21 +0000 | danse-nr3 | (~danse-nr3@user/danse-nr3) |
| 2024-07-16 15:42:28 +0000 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
| 2024-07-16 15:43:46 +0000 | ystael | (~ystael@user/ystael) (Ping timeout: 248 seconds) |
| 2024-07-16 15:44:51 +0000 | ystael | (~ystael@user/ystael) |
| 2024-07-16 15:45:07 +0000 | ash3en | (~ash3en@89.246.174.164) (Remote host closed the connection) |
| 2024-07-16 15:52:51 +0000 | <haskellbridge> | <thirdofmay18081814goya> what's your preferred approach to refinement types in haskell? |
| 2024-07-16 15:52:54 +0000 | <haskellbridge> | <thirdofmay18081814goya> liquid haskell? |
| 2024-07-16 15:54:18 +0000 | <EvanR> | smart constructors |
| 2024-07-16 15:55:00 +0000 | <EvanR> | liquid haskell is another language |
| 2024-07-16 16:05:24 +0000 | <haskellbridge> | <thirdofmay18081814goya> EvanR: hm, you can't call these in type declarations |
| 2024-07-16 16:05:50 +0000 | <haskellbridge> | <thirdofmay18081814goya> +(if you want to use refinement types to declare other types) |
| 2024-07-16 16:05:59 +0000 | <EvanR> | in liquid haskell? |
| 2024-07-16 16:06:10 +0000 | mikess | (~mikess@user/mikess) |
| 2024-07-16 16:06:24 +0000 | <haskellbridge> | <thirdofmay18081814goya> no in standard haskell |
| 2024-07-16 16:08:37 +0000 | <EvanR> | haskell doesn't have refinement types |
| 2024-07-16 16:10:58 +0000 | CiaoSen | (~Jura@2a05:5800:2b3:5600:e6b9:7aff:fe80:3d03) (Ping timeout: 248 seconds) |
| 2024-07-16 16:16:06 +0000 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 272 seconds) |
| 2024-07-16 16:16:11 +0000 | albet70 | (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Server closed connection) |
| 2024-07-16 16:17:54 +0000 | dolio | (~dolio@130.44.140.168) |
| 2024-07-16 16:19:52 +0000 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
| 2024-07-16 16:23:14 +0000 | albet70 | (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 2024-07-16 16:27:14 +0000 | Apollyon | (~Apollyon@user/Apollyon) |
| 2024-07-16 16:27:29 +0000 | danse-nr3 | (~danse-nr3@user/danse-nr3) (Ping timeout: 248 seconds) |
| 2024-07-16 16:29:33 +0000 | Athas | (athas@sigkill.dk) (Server closed connection) |
| 2024-07-16 16:31:06 +0000 | ames | (~amelia@offtopia/offtopian/amelia) (Server closed connection) |
| 2024-07-16 16:31:07 +0000 | Athas | (athas@2a01:7c8:aaac:1cf:43b5:af0:11ab:b009) |
| 2024-07-16 16:31:18 +0000 | ames | (~amelia@offtopia/offtopian/amelia) |
| 2024-07-16 16:32:41 +0000 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-07-16 16:34:45 +0000 | tomku | (~tomku@user/tomku) (Ping timeout: 246 seconds) |
| 2024-07-16 16:38:51 +0000 | manwithluck | (manwithluc@gateway/vpn/protonvpn/manwithluck) (Server closed connection) |
| 2024-07-16 16:39:18 +0000 | manwithluck | (manwithluc@gateway/vpn/protonvpn/manwithluck) |
| 2024-07-16 16:40:27 +0000 | cpressey | (~weechat@176.254.71.203) (Ping timeout: 252 seconds) |
| 2024-07-16 16:41:35 +0000 | tomku | (~tomku@user/tomku) |
| 2024-07-16 16:45:10 +0000 | danse-nr3 | (~danse-nr3@user/danse-nr3) |
| 2024-07-16 16:46:53 +0000 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 244 seconds) |
| 2024-07-16 16:54:08 +0000 | phma | (~phma@host-67-44-208-24.hnremote.net) (Read error: Connection reset by peer) |
| 2024-07-16 16:57:53 +0000 | Square2 | (~Square@user/square) (Ping timeout: 248 seconds) |
| 2024-07-16 16:59:35 +0000 | ft | (~ft@p4fc2ab80.dip0.t-ipconnect.de) |
| 2024-07-16 17:03:00 +0000 | danse-nr3 | (~danse-nr3@user/danse-nr3) (Ping timeout: 252 seconds) |
| 2024-07-16 17:06:49 +0000 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2024-07-16 17:12:38 +0000 | misterfish | (~misterfis@84.53.85.146) |
| 2024-07-16 17:12:54 +0000 | phma | (~phma@host-67-44-208-140.hnremote.net) |
| 2024-07-16 17:22:54 +0000 | <amjoseph> | tromp thanks for posting that! would never have expected that the [sequence whose limit is the] proof-theoretic ordinal for CoC can be computed by such a short program. i'm a bit surprised, however, that they didn't *prove* that it actually computes that. you should be able to prove it in coq since iirc CiC has strictly greater consistency strength. anyways, TIL; thanks. |
| 2024-07-16 17:23:05 +0000 | ash3en | (~ash3en@2a02:3100:7db2:6b01:4f69:739c:8091:4c20) |
| 2024-07-16 17:23:58 +0000 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-07-16 17:25:36 +0000 | <amjoseph> | tromp (also) maybe try asking sridhar ramesh? |
| 2024-07-16 17:27:44 +0000 | rosco | (~rosco@175.136.155.137) (Quit: Lost terminal) |
| 2024-07-16 17:28:02 +0000 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-07-16 17:32:05 +0000 | danse-nr3 | (~danse-nr3@user/danse-nr3) |
| 2024-07-16 17:37:06 +0000 | danse-nr3 | (~danse-nr3@user/danse-nr3) (Ping timeout: 252 seconds) |
| 2024-07-16 17:37:37 +0000 | destituion | (~destituio@2001:4644:c37:0:5095:eb5b:7529:4c8f) |
| 2024-07-16 17:38:13 +0000 | danse-nr3 | (~danse-nr3@user/danse-nr3) |
| 2024-07-16 17:40:34 +0000 | AlexZenon | (~alzenon@178.34.160.117) (Ping timeout: 248 seconds) |
| 2024-07-16 17:40:56 +0000 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-07-16 17:44:44 +0000 | infinity0_ | (~infinity0@pwned.gg) |
| 2024-07-16 17:45:08 +0000 | AlexZenon | (~alzenon@178.34.160.117) |
| 2024-07-16 17:45:52 +0000 | infinity0 | (~infinity0@pwned.gg) (Ping timeout: 246 seconds) |
| 2024-07-16 17:47:00 +0000 | misterfish | (~misterfis@84.53.85.146) (Ping timeout: 252 seconds) |
| 2024-07-16 17:51:49 +0000 | misterfish | (~misterfis@84.53.85.146) |
| 2024-07-16 17:55:51 +0000 | <mauke> | :t \x y -> ?f x y <= EQ |
| 2024-07-16 17:55:52 +0000 | <lambdabot> | (?f::t1 -> t2 -> Ordering) => t1 -> t2 -> Bool |
| 2024-07-16 17:56:21 +0000 | zfnmxt | (~zfnmxt@user/zfnmxt) (Server closed connection) |
| 2024-07-16 17:56:39 +0000 | zfnmxt | (~zfnmxt@user/zfnmxt) |
| 2024-07-16 17:56:48 +0000 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 272 seconds) |
| 2024-07-16 18:02:02 +0000 | wagle | (~wagle@quassel.wagle.io) (Server closed connection) |
| 2024-07-16 18:02:17 +0000 | wagle | (~wagle@quassel.wagle.io) |
| 2024-07-16 18:18:57 +0000 | misterfish | (~misterfis@84.53.85.146) (Ping timeout: 248 seconds) |
| 2024-07-16 18:21:19 +0000 | ash3en | (~ash3en@2a02:3100:7db2:6b01:4f69:739c:8091:4c20) (Ping timeout: 256 seconds) |
| 2024-07-16 18:24:18 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 246 seconds) |
| 2024-07-16 18:25:12 +0000 | misterfish | (~misterfis@84.53.85.146) |
| 2024-07-16 18:25:56 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) |
| 2024-07-16 18:33:53 +0000 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2024-07-16 18:35:41 +0000 | doyougnu | (~doyougnu@syn-045-046-170-068.res.spectrum.com) (Server closed connection) |
| 2024-07-16 18:35:57 +0000 | doyougnu | (~doyougnu@syn-045-046-170-068.res.spectrum.com) |
| 2024-07-16 18:38:46 +0000 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2024-07-16 18:39:03 +0000 | califax | (~califax@user/califx) |
| 2024-07-16 18:40:54 +0000 | Apollyon | (~Apollyon@user/Apollyon) (Remote host closed the connection) |
| 2024-07-16 18:41:18 +0000 | jespada | (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Server closed connection) |
| 2024-07-16 18:44:30 +0000 | cpressey | (~weechat@176.254.71.203) |
| 2024-07-16 18:46:29 +0000 | gmg | (~user@user/gehmehgeh) |
| 2024-07-16 18:46:51 +0000 | jespada | (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) |
| 2024-07-16 18:49:57 +0000 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-07-16 18:53:11 +0000 | koz | (~koz@121.99.240.58) (Server closed connection) |
| 2024-07-16 18:53:27 +0000 | koz | (~koz@121.99.240.58) |
| 2024-07-16 18:54:51 +0000 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2024-07-16 18:54:53 +0000 | <stefan-__> | is it possible to check if a FilePath exists (and if not show an error) when extracting CLI params via optparse-applicative? |
| 2024-07-16 18:57:23 +0000 | Angelz | (Angelz@user/angelz) (Server closed connection) |
| 2024-07-16 18:59:06 +0000 | <mud> | stefan-__: Not saying you definitely shouldn't do that, but: be careful of the pattern of check-first for files. It leads to race conditions, things can change between when you check and when you actually use it. |
| 2024-07-16 18:59:23 +0000 | <mud> | You're usually better off just dealing with the error _as_ you use the file, because you're going to have to do it there anyway. |
| 2024-07-16 19:01:47 +0000 | ash3en | (~ash3en@2a02:3100:7db2:6b01:4f69:739c:8091:4c20) |
| 2024-07-16 19:02:32 +0000 | bearen | (Thunderbir@user/bearen) |
| 2024-07-16 19:08:01 +0000 | Angelz | (Angelz@Angelz.oddprotocol.org) |
| 2024-07-16 19:09:48 +0000 | simendsjo | (~user@31-209-41-70.cust.bredband2.com) |
| 2024-07-16 19:15:31 +0000 | euphores | (~SASL_euph@user/euphores) |
| 2024-07-16 19:19:04 +0000 | Maeda | (~Maeda@91-161-10-149.subs.proxad.net) (Quit: leaving) |
| 2024-07-16 19:19:05 +0000 | c_wraith | (~c_wraith@adjoint.us) (Server closed connection) |
| 2024-07-16 19:20:15 +0000 | c_wraith | (~c_wraith@adjoint.us) |
| 2024-07-16 19:21:58 +0000 | <EvanR> | boldly open the file and if there is a reasonable thing to do other than crash in case of a problem, catch the specific exception |
| 2024-07-16 19:24:01 +0000 | <EvanR> | or in a more complicated application, check the result of the async thread tasked with doing something with that file |
| 2024-07-16 19:25:00 +0000 | danse-nr3 | (~danse-nr3@user/danse-nr3) (Read error: Connection reset by peer) |
| 2024-07-16 19:25:30 +0000 | danse-nr3 | (~danse-nr3@user/danse-nr3) |
| 2024-07-16 19:27:06 +0000 | destituion | (~destituio@2001:4644:c37:0:5095:eb5b:7529:4c8f) (Ping timeout: 252 seconds) |
| 2024-07-16 19:27:48 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-07-16 19:29:33 +0000 | destituion | (~destituio@2a02:2121:6b6:b142:8d9d:8eb3:8da8:98dd) |
| 2024-07-16 19:59:36 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2024-07-16 20:01:48 +0000 | danse-nr3 | (~danse-nr3@user/danse-nr3) (Quit: Leaving) |
| 2024-07-16 20:16:21 +0000 | mreh | (~matthew@host86-160-168-12.range86-160.btcentralplus.com) |
| 2024-07-16 20:17:51 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-07-16 20:24:41 +0000 | A_Dragon | (A_D@libera/staff/dragon) (Quit: ZNC - https://znc.in) |
| 2024-07-16 20:24:56 +0000 | A_Dragon | (A_D@libera/staff/dragon) |
| 2024-07-16 20:25:23 +0000 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-07-16 20:25:41 +0000 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2024-07-16 20:27:10 +0000 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-07-16 20:29:17 +0000 | <stefan-__> | mud + EvanR: thanks, maybe this even better fits separation of concerns, in the way that optparse-applicative is really only used for CLI param parsing |
| 2024-07-16 20:30:23 +0000 | <raehik> | I want to sort a list-like `f a`. I have an `a -> a -> Ordering`. Is there a way I can do this polymorphically over `f`? |
| 2024-07-16 20:31:07 +0000 | <ncf> | raehik: https://elvishjerricco.github.io/2017/03/23/applicative-sorting.html ? |
| 2024-07-16 20:31:37 +0000 | <mreh> | what about using Foldable? |
| 2024-07-16 20:32:30 +0000 | <raehik> | mreh: Foldable is for folding operations. I don't want to fold the list to a single value |
| 2024-07-16 20:32:36 +0000 | tomku | (~tomku@user/tomku) (Ping timeout: 272 seconds) |
| 2024-07-16 20:32:40 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2024-07-16 20:32:44 +0000 | <raehik> | I can't see an `f a -> f a` operation in Foldable |
| 2024-07-16 20:32:47 +0000 | <mreh> | :t toList |
| 2024-07-16 20:32:48 +0000 | <lambdabot> | Foldable t => t a -> [a] |
| 2024-07-16 20:32:51 +0000 | tomku | (~tomku@user/tomku) |
| 2024-07-16 20:33:10 +0000 | <mreh> | half way there |
| 2024-07-16 20:33:29 +0000 | <ncf> | you obviously need Traversable |
| 2024-07-16 20:33:45 +0000 | <ncf> | or something equivalent |
| 2024-07-16 20:34:14 +0000 | <raehik> | mreh: this lets me sort `f a`, but at the cost of going between List, which isn't really what I was looking for |
| 2024-07-16 20:34:27 +0000 | <mreh> | raehik: listen to ncf |
| 2024-07-16 20:34:44 +0000 | simendsjo | (~user@31-209-41-70.cust.bredband2.com) (Ping timeout: 244 seconds) |
| 2024-07-16 20:34:49 +0000 | <raehik> | ncf: thanks for that, looks interesting! |
| 2024-07-16 20:34:52 +0000 | <mreh> | You want to substitute elements in the functor for each other, traversable sounds like a good fit to me |
| 2024-07-16 20:37:33 +0000 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-07-16 20:38:00 +0000 | <raehik> | my thought process was "what if I had a `Vector a` and wanted to sort it quickly", but... I can't see a sort op in the vector package. huh |
| 2024-07-16 20:39:34 +0000 | mreh | wonders how does one update a collection using multiple concurrent `Event (f a -> f a)`s in reflex... |
| 2024-07-16 20:39:46 +0000 | <mreh> | raehik: what flavour of Vector? |
| 2024-07-16 20:40:05 +0000 | <mreh> | and what does quickly mean? |
| 2024-07-16 20:40:16 +0000 | <raehik> | Any, say Primitive |
| 2024-07-16 20:40:40 +0000 | CiaoSen | (~Jura@2a05:5800:2b3:5600:e6b9:7aff:fe80:3d03) |
| 2024-07-16 20:40:53 +0000 | <raehik> | quickly as in init a new vector of the same size and write into it |
| 2024-07-16 20:41:39 +0000 | <mreh> | I would just convert between Vector a and [a] and back again probably |
| 2024-07-16 20:41:53 +0000 | <raehik> | perhaps stream fusion permits simply going through List |
| 2024-07-16 20:42:10 +0000 | <haskellbridge> | <Jade> `vector-algorithms` has fast sorts |
| 2024-07-16 20:42:12 +0000 | connrs | (~connrs@user/connrs) (Server closed connection) |
| 2024-07-16 20:42:28 +0000 | connrs | (~connrs@user/connrs) |
| 2024-07-16 20:42:56 +0000 | <raehik> | Ah! yes, fantastic. I knew of that pkg too haha |
| 2024-07-16 20:43:03 +0000 | <raehik> | it does in-place sorts so hard to Hoogle |
| 2024-07-16 20:44:47 +0000 | it_ | (~quassel@v2202212189510211193.supersrv.de) (Server closed connection) |
| 2024-07-16 20:44:55 +0000 | it_ | (~quassel@v2202212189510211193.supersrv.de) |
| 2024-07-16 20:49:54 +0000 | cpressey | (~weechat@176.254.71.203) (Ping timeout: 248 seconds) |
| 2024-07-16 20:51:30 +0000 | pieguy128 | (~pieguy128@bras-base-mtrlpq5031w-grc-45-67-70-24-166.dsl.bell.ca) (Server closed connection) |
| 2024-07-16 20:52:54 +0000 | pieguy128 | (~pieguy128@bras-base-mtrlpq5031w-grc-45-67-70-24-166.dsl.bell.ca) |
| 2024-07-16 20:55:24 +0000 | mreh | (~matthew@host86-160-168-12.range86-160.btcentralplus.com) (Ping timeout: 244 seconds) |
| 2024-07-16 20:55:28 +0000 | <raehik> | I've used mutable vectors before and I still had to search around to confirm how to do basic things (`modify`)... |
| 2024-07-16 21:02:09 +0000 | misterfish | (~misterfis@84.53.85.146) (Ping timeout: 248 seconds) |
| 2024-07-16 21:02:10 +0000 | AlexZenon | (~alzenon@178.34.160.117) (Ping timeout: 248 seconds) |
| 2024-07-16 21:03:06 +0000 | <raehik> | it'd also be nice if vector-algorithms endorsed certain sorts for different usages. I had to go through each module to check docs instead. perhaps that's the intended experience but felt a bit long-winded |
| 2024-07-16 21:04:29 +0000 | emmanuelux | (~emmanuelu@user/emmanuelux) |
| 2024-07-16 21:09:38 +0000 | ash3en | (~ash3en@2a02:3100:7db2:6b01:4f69:739c:8091:4c20) (Remote host closed the connection) |
| 2024-07-16 21:09:46 +0000 | <EvanR> | haskell is fairly far down the road from "just sort my list-like thing I don't care how you do it" |
| 2024-07-16 21:10:00 +0000 | <EvanR> | starting with how there's no generic "list-like" data structure |
| 2024-07-16 21:10:01 +0000 | ash3en | (~ash3en@2a02:3100:7db2:6b01:4f69:739c:8091:4c20) |
| 2024-07-16 21:10:30 +0000 | <EvanR> | you have to decide what string, what number, what whatever based on whether you're optimizing engineering effort or performance for the task |
| 2024-07-16 21:10:32 +0000 | AlexZenon | (~alzenon@178.34.160.117) |
| 2024-07-16 21:11:43 +0000 | ash3en | (~ash3en@2a02:3100:7db2:6b01:4f69:739c:8091:4c20) (Remote host closed the connection) |
| 2024-07-16 21:13:43 +0000 | <raehik> | EvanR: Right, I agree. vector-algos gives many options for sorting |
| 2024-07-16 21:14:20 +0000 | <raehik> | I was lamenting the lack of any package preamble or introduction. I don't want a button that says "just use this", I was hoping for a general overview |
| 2024-07-16 21:15:21 +0000 | <raehik> | (perhaps you were looking at earlier messages, I was specifically keen on Vectors now) |
| 2024-07-16 21:17:20 +0000 | <monochrom> | There is the issue of having heard of vector-algorithms in the first place. But suppose we're past that, then maybe you haven't seen the life hack of: click on any module, then click on "Index". |
| 2024-07-16 21:18:03 +0000 | <monochrom> | BTW I also wish the "Index" link were on the package front page on hackage. |
| 2024-07-16 21:20:04 +0000 | <tomsmeding> | monochrom: it is |
| 2024-07-16 21:20:09 +0000 | <tomsmeding> | [Index] under Modules |
| 2024-07-16 21:20:49 +0000 | <monochrom> | Ugh OK now I see but it's ant-size that's why I never saw it. |
| 2024-07-16 21:21:21 +0000 | AlexZenon | (~alzenon@178.34.160.117) (Ping timeout: 248 seconds) |
| 2024-07-16 21:21:22 +0000 | <tomsmeding> | I myself am quite partial to Quick Jump, which is also brought up if you press the 's' key on the keyboard on any module page (and, for many packages -- but apparently not this one -- on the package front page) |
| 2024-07-16 21:21:53 +0000 | <tomsmeding> | I found the link by searching for "index" on the page :p |
| 2024-07-16 21:23:50 +0000 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-07-16 21:25:44 +0000 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2024-07-16 21:25:49 +0000 | AlexZenon | (~alzenon@178.34.160.117) |
| 2024-07-16 21:26:43 +0000 | <raehik> | monochrom: if that's the intended experience then all good I suppose. individual modules have great docs but the user is apparently expected to click around until they're happy with the algo they find |
| 2024-07-16 21:27:23 +0000 | <raehik> | I was hoping for some benches and high-level notes. not actively complaining or searching for a fix |
| 2024-07-16 21:27:32 +0000 | <monochrom> | I don't think it's intended. But I think people trust too much into hierarchies. |
| 2024-07-16 21:28:00 +0000 | <raehik> | monochrom: as in module hierarchies? unclear what you mean |
| 2024-07-16 21:30:09 +0000 | <monochrom> | OK let me describe my own dilemma. I teach multiple courses, over multiple semesters. Should my directory tree structure be "semester/course" or should it be "course/semester"? (Answer: "tree" is already wrong right there. Should be a matrix.) |
| 2024-07-16 21:31:41 +0000 | <monochrom> | I even sometimes torment my C-and-Unix students with: "The prof was using the former but now changes his mind and wants to migrate to the latter! Write a shell script for that..." |
| 2024-07-16 21:31:43 +0000 | <raehik> | you're absolutely right I hate hierarchies too. we need a filesystem based on tag matrices NOW |
| 2024-07-16 21:33:31 +0000 | <raehik> | the current answer is, sadly, an overabundance of symlinks |
| 2024-07-16 21:33:51 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-07-16 21:36:56 +0000 | cpressey | (~weechat@176.254.71.203) |
| 2024-07-16 21:37:28 +0000 | infinity0_ | (~infinity0@pwned.gg) (Remote host closed the connection) |
| 2024-07-16 21:37:51 +0000 | infinity0 | (~infinity0@pwned.gg) |
| 2024-07-16 21:40:19 +0000 | Vajb | (~Vajb@n84f8idehd0ucclhxoj-1.v6.elisa-mobile.fi) (Ping timeout: 264 seconds) |
| 2024-07-16 21:40:35 +0000 | Vajb | (~Vajb@n85jaspk9c2pfwcdhy6-1.v6.elisa-mobile.fi) |
| 2024-07-16 21:46:47 +0000 | cpressey | (~weechat@176.254.71.203) (Quit: WeeChat 4.3.0) |
| 2024-07-16 21:47:20 +0000 | ddellacosta | (~ddellacos@ool-44c73d29.dyn.optonline.net) |
| 2024-07-16 21:48:37 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2024-07-16 21:51:46 +0000 | acidjnk | (~acidjnk@p200300d6e72cfb805cd63c25806f679d.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 2024-07-16 21:59:45 +0000 | ystael | (~ystael@user/ystael) (Ping timeout: 248 seconds) |
| 2024-07-16 22:04:32 +0000 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) |
| 2024-07-16 22:05:00 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Read error: Connection reset by peer) |
| 2024-07-16 22:07:28 +0000 | Lord_of_Life_ | Lord_of_Life |
| 2024-07-16 22:17:02 +0000 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 244 seconds) |
| 2024-07-16 22:17:04 +0000 | Sgeo | (~Sgeo@user/sgeo) |
| 2024-07-16 22:20:22 +0000 | CiaoSen | (~Jura@2a05:5800:2b3:5600:e6b9:7aff:fe80:3d03) (Ping timeout: 252 seconds) |
| 2024-07-16 22:32:50 +0000 | euleritian | (~euleritia@dynamic-176-005-135-121.176.5.pool.telefonica.de) (Ping timeout: 248 seconds) |
| 2024-07-16 22:35:19 +0000 | euleritian | (~euleritia@dynamic-176-005-134-181.176.5.pool.telefonica.de) |
| 2024-07-16 22:40:58 +0000 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2024-07-16 22:45:11 +0000 | pavonia | (~user@user/siracusa) |
| 2024-07-16 23:08:05 +0000 | andrea_r | (~user@93-49-96-212.ip366.fastwebnet.it) (Ping timeout: 252 seconds) |
| 2024-07-16 23:16:29 +0000 | CrunchyFlakes | (~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-07-16 23:19:07 +0000 | CrunchyFlakes | (~CrunchyFl@146.52.130.128) |
| 2024-07-16 23:34:41 +0000 | oo_miguel | (~Thunderbi@78.10.207.46) (Ping timeout: 265 seconds) |
| 2024-07-16 23:36:50 +0000 | dunj3 | (~dunj3@kingdread.de) (Server closed connection) |
| 2024-07-16 23:37:55 +0000 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-07-16 23:38:01 +0000 | dunj3 | (~dunj3@kingdread.de) |
| 2024-07-16 23:39:56 +0000 | mzg | (mzg@abusers.hu) (Server closed connection) |
| 2024-07-16 23:40:00 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-07-16 23:40:02 +0000 | mzg | (mzg@abusers.hu) |
| 2024-07-16 23:46:25 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2024-07-16 23:51:18 +0000 | Me-me | (~me-me@kc.randomserver.name) (Server closed connection) |
| 2024-07-16 23:53:52 +0000 | Me-me | (~me-me@kc.randomserver.name) |
| 2024-07-16 23:57:50 +0000 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 2024-07-16 23:58:18 +0000 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
| 2024-07-16 23:59:16 +0000 | dysthesis | (~dysthesis@user/dysthesis) |