Newest at the top
| 2025-07-16 18:22:28 +0200 | caubert | (~caubert@user/caubert) (Ping timeout: 276 seconds) |
| 2025-07-16 18:19:31 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2025-07-16 18:19:06 +0200 | fp | (~Thunderbi@89-209-68-31.mobile.vf-ua.net) fp |
| 2025-07-16 18:17:11 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 2025-07-16 18:13:43 +0200 | notzmv | (~umar@user/notzmv) (Ping timeout: 245 seconds) |
| 2025-07-16 18:12:38 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection) |
| 2025-07-16 18:06:28 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess |
| 2025-07-16 18:04:23 +0200 | acidjnk | (~acidjnk@p200300d6e70b66275c4a48d94f205259.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2025-07-16 18:04:06 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) chexum |
| 2025-07-16 18:03:46 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) (Ping timeout: 244 seconds) |
| 2025-07-16 18:03:17 +0200 | tromp | (~textual@2001:1c00:3487:1b00:a9b1:9c68:1be8:4e5d) |
| 2025-07-16 18:02:14 +0200 | Square | (~Square@user/square) (Ping timeout: 260 seconds) |
| 2025-07-16 17:59:03 +0200 | dtman34 | (~dtman34@2601:447:d182:6512:c2f9:c3a:b83d:6490) dtman34 |
| 2025-07-16 17:58:29 +0200 | dtman34 | (~dtman34@c-73-242-68-179.hsd1.mn.comcast.net) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 2025-07-16 17:53:27 +0200 | dtman34 | (~dtman34@c-73-242-68-179.hsd1.mn.comcast.net) dtman34 |
| 2025-07-16 17:44:46 +0200 | athan | (~athan@syn-047-132-161-157.res.spectrum.com) athan |
| 2025-07-16 17:44:04 +0200 | prdak | (~Thunderbi@user/prdak) (Read error: Connection reset by peer) |
| 2025-07-16 17:43:45 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-07-16 17:42:18 +0200 | tromp | (~textual@2001:1c00:3487:1b00:207a:b700:e4:7b01) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-07-16 17:37:45 +0200 | ttybitnik | (~ttybitnik@user/wolper) (Remote host closed the connection) |
| 2025-07-16 17:35:37 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 2025-07-16 17:34:27 +0200 | dtman34 | (~dtman34@2601:447:d182:6512:c2f9:c3a:b83d:6490) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 2025-07-16 17:33:09 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-07-16 17:26:52 +0200 | trickard_ | (~trickard@cpe-50-98-47-163.wireline.com.au) |
| 2025-07-16 17:26:39 +0200 | trickard | (~trickard@cpe-50-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-07-16 17:24:49 +0200 | ski | . o O ( `test (null -> case s of {"empty" -> False ; "not empty" -> True })) = s' ) |
| 2025-07-16 17:20:49 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
| 2025-07-16 17:19:53 +0200 | Frostillicus | (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) |
| 2025-07-16 17:18:55 +0200 | dtman34 | (~dtman34@2601:447:d182:6512:c2f9:c3a:b83d:6490) dtman34 |
| 2025-07-16 17:18:24 +0200 | dtman34 | (~dtman34@2601:447:d182:6512:c2f9:c3a:b83d:6490) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 2025-07-16 17:17:46 +0200 | caubert | (~caubert@user/caubert) caubert |
| 2025-07-16 17:16:46 +0200 | Frostillicus | (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) (Read error: Connection reset by peer) |
| 2025-07-16 17:15:42 +0200 | Everything | (~Everythin@46.211.88.66) Everything |
| 2025-07-16 17:14:26 +0200 | prdak | (~Thunderbi@user/prdak) prdak |
| 2025-07-16 17:13:48 +0200 | Everything | (~Everythin@5.248.237.239) (Ping timeout: 252 seconds) |
| 2025-07-16 17:11:18 +0200 | Frostillicus | (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) |
| 2025-07-16 17:07:52 +0200 | Frostillicus | (~Frostilli@pool-71-174-119-69.bstnma.fios.verizon.net) (Read error: Connection reset by peer) |
| 2025-07-16 17:05:53 +0200 | caubert | (~caubert@user/caubert) (Ping timeout: 248 seconds) |
| 2025-07-16 17:04:28 +0200 | <lambdabot> | ["not empty","empty","empty"] |
| 2025-07-16 17:04:26 +0200 | <ski> | > let ((. null) -> test) = \case False -> "empty"; True -> "not empty" in map test ["","a","bc"] -- this is another option, absence. looks kinda weird, though |
| 2025-07-16 17:02:56 +0200 | <ski> | would look pretty neat |
| 2025-07-16 17:02:51 +0200 | <ski> | test (null -> True ) = "not empty" |
| 2025-07-16 17:02:45 +0200 | <ski> | test (null -> False) = "empty" |
| 2025-07-16 17:02:34 +0200 | <ski> | but |
| 2025-07-16 17:01:50 +0200 | <ski> | test xs | True = "not empty" |
| 2025-07-16 17:01:40 +0200 | <ski> | test xs | False = "empty" |
| 2025-07-16 17:01:21 +0200 | <ski> | test xs with null xs |
| 2025-07-16 17:01:02 +0200 | <ski> | in Agda, you have `with' patterns, which imply a single call |
| 2025-07-16 17:00:17 +0200 | <ski> | and i know GHC often doesn't want to do CSE, in order to avoid introducing space leaks |
| 2025-07-16 17:00:08 +0200 | dtman34 | (~dtman34@2601:447:d182:6512:c2f9:c3a:b83d:6490) dtman34 |