Newest at the top
| 2025-12-04 13:47:50 +0100 | divya | (divya@140.238.251.170) divya |
| 2025-12-04 13:46:18 +0100 | lambda_gibbon | (~lambda_gi@2603:7080:ee00:37d8:313d:1898:c3f8:5287) |
| 2025-12-04 13:41:11 +0100 | img | (~img@user/img) img |
| 2025-12-04 13:41:09 +0100 | xff0x | (~xff0x@2405:6580:b080:900:d454:e7ea:27f9:454f) |
| 2025-12-04 13:39:56 +0100 | img | (~img@user/img) (Quit: ZNC 1.10.1 - https://znc.in) |
| 2025-12-04 13:39:35 +0100 | <lucabtz> | im confused on how to go from value level to type level though, if it even is possible |
| 2025-12-04 13:38:21 +0100 | <lucabtz> | yeah i might change to that |
| 2025-12-04 13:36:35 +0100 | ljdarj1 | ljdarj |
| 2025-12-04 13:36:35 +0100 | Ging_ | (46fea76d80@2001:bc8:1210:2cd8::470) (Ping timeout: 245 seconds) |
| 2025-12-04 13:36:35 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 240 seconds) |
| 2025-12-04 13:36:32 +0100 | hdggxin | (~hdggxin@2401:4900:88a9:bff0:be1a:791c:4871:3d3b) (Remote host closed the connection) |
| 2025-12-04 13:35:02 +0100 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-12-04 13:35:01 +0100 | PaulMartensen | (2c15493d69@2001:bc8:1210:2cd8::3bc) (Ping timeout: 255 seconds) |
| 2025-12-04 13:34:41 +0100 | Typosit | (b41a81e702@2001:bc8:1210:2cd8::494) (Ping timeout: 244 seconds) |
| 2025-12-04 13:30:21 +0100 | Typosit | (b41a81e702@2001:bc8:1210:2cd8::494) |
| 2025-12-04 13:30:20 +0100 | Ging_ | (46fea76d80@2001:bc8:1210:2cd8::470) |
| 2025-12-04 13:30:20 +0100 | PaulMartensen | (2c15493d69@2001:bc8:1210:2cd8::3bc) |
| 2025-12-04 13:29:44 +0100 | X-Scale | (~ARM@50.65.114.89.rev.vodafone.pt) (Ping timeout: 240 seconds) |
| 2025-12-04 13:29:00 +0100 | Typosit | (b41a81e702@2001:bc8:1210:2cd8::494) (Remote host closed the connection) |
| 2025-12-04 13:29:00 +0100 | Ging_ | (46fea76d80@2001:bc8:1210:2cd8::470) (Remote host closed the connection) |
| 2025-12-04 13:29:00 +0100 | PaulMartensen | (15a119e437@2001:bc8:1210:2cd8::3bc) (Remote host closed the connection) |
| 2025-12-04 13:27:39 +0100 | <tomsmeding> | consider changing the <= to < |
| 2025-12-04 13:27:29 +0100 | <tomsmeding> | this need not be a problem at all, but I find that things work a bit more nicely if you keep to the convention "lower bounds are inclusive, upper bounds are exclusive" |
| 2025-12-04 13:27:18 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-12-04 13:27:06 +0100 | <tomsmeding> | so there is kind of one natural case that you cannot express |
| 2025-12-04 13:26:57 +0100 | <tomsmeding> | lucabtz: with the <= bound it's impossible to hvae an "impossible" BoundedNatural |
| 2025-12-04 13:26:32 +0100 | <tomsmeding> | names are a little long, but that's personal :p |
| 2025-12-04 13:26:25 +0100 | <tomsmeding> | yes |
| 2025-12-04 13:24:29 +0100 | trickard_ | (~trickard@cpe-85-98-47-163.wireline.com.au) |
| 2025-12-04 13:24:15 +0100 | trickard_ | (~trickard@cpe-85-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-12-04 13:21:10 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 245 seconds) |
| 2025-12-04 13:19:20 +0100 | wbooze | (~wbooze@2001-4dd4-1daa-0-acf3-bea0-8250-a5a2.ipv6dyn.netcologne.de) Inline |
| 2025-12-04 13:12:41 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-12-04 13:12:30 +0100 | <lucabtz> | https://paste.tomsmeding.com/blBvVp0I does this make any sense to you? |
| 2025-12-04 13:05:22 +0100 | srazkvt | (~sarah@user/srazkvt) srazkvt |
| 2025-12-04 13:02:58 +0100 | __monty__ | (~toonn@user/toonn) toonn |
| 2025-12-04 13:00:23 +0100 | wbooze | (~wbooze@cgn-195-14-220-195.nc.de) (Quit: Leaving) |
| 2025-12-04 12:59:44 +0100 | trickard_ | (~trickard@cpe-85-98-47-163.wireline.com.au) |
| 2025-12-04 12:59:30 +0100 | trickard | (~trickard@cpe-85-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-12-04 12:57:40 +0100 | karenw | (~karenw@user/karenw) (Ping timeout: 255 seconds) |
| 2025-12-04 12:39:51 +0100 | annamalai | (~annamalai@157.32.217.175) (Ping timeout: 265 seconds) |
| 2025-12-04 12:38:59 +0100 | DetourNetworkUK | (~DetourNet@user/DetourNetworkUK) DetourNetworkUK |
| 2025-12-04 12:28:49 +0100 | xff0x | (~xff0x@fs98a57788.tkyc008.ap.nuro.jp) (Ping timeout: 264 seconds) |
| 2025-12-04 12:26:15 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) chromoblob\0 |
| 2025-12-04 12:23:23 +0100 | fp | (~Thunderbi@130.233.70.22) fp |
| 2025-12-04 12:17:25 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 264 seconds) |
| 2025-12-04 12:16:35 +0100 | DetourNetworkUK | (~DetourNet@user/DetourNetworkUK) (Ping timeout: 245 seconds) |
| 2025-12-04 12:09:53 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) (Ping timeout: 260 seconds) |
| 2025-12-04 12:08:50 +0100 | Square2 | (~Square4@user/square) (Quit: Leaving) |
| 2025-12-04 12:05:45 +0100 | poscat | (~poscat@user/poscat) (Ping timeout: 245 seconds) |