Newest at the top
2025-08-08 15:58:23 +0200 | Cale | (~cale@2607:fea8:995f:f126:15c3:35a5:81ac:187c) Cale |
2025-08-08 15:51:31 +0200 | smiesner | (b0cf5acf8c@user/smiesner) smiesner |
2025-08-08 15:51:24 +0200 | smiesner | (b0cf5acf8c@user/smiesner) (Server closed connection) |
2025-08-08 15:48:14 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
2025-08-08 15:47:30 +0200 | jespada | (~jespada@2800:a4:2228:2400:e5a0:dd56:e91c:d25b) jespada |
2025-08-08 15:39:04 +0200 | jespada | (~jespada@r179-25-146-183.dialup.adsl.anteldata.net.uy) (Quit: Textual IRC Client: www.textualapp.com) |
2025-08-08 15:37:59 +0200 | statusfailed | (~statusfai@statusfailed.com) () |
2025-08-08 15:36:54 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
2025-08-08 15:24:17 +0200 | sprotte24 | (~sprotte24@p200300d16f43d3003d43dd3d16486e1e.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
2025-08-08 15:23:18 +0200 | dyniec | (~dyniec@dybiec.info) |
2025-08-08 15:22:41 +0200 | dyniec | (~dyniec@dybiec.info) (Remote host closed the connection) |
2025-08-08 15:22:40 +0200 | AlexZenon | (~alzenon@178.34.162.188) |
2025-08-08 15:21:57 +0200 | Vajb | (~Vajb@n4ff0xajgx7huazq3a1-1.v6.elisa-mobile.fi) (Ping timeout: 248 seconds) |
2025-08-08 15:21:02 +0200 | AlexNoo | (~AlexNoo@178.34.162.188) |
2025-08-08 15:05:35 +0200 | statusfailed | (~statusfai@statusfailed.com) statusfailed |
2025-08-08 15:02:58 +0200 | haritz | (~hrtz@user/haritz) haritz |
2025-08-08 15:02:58 +0200 | haritz | (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) (Changing host) |
2025-08-08 15:02:58 +0200 | haritz | (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) |
2025-08-08 15:00:24 +0200 | Lycurgus | (~juan@user/Lycurgus) (Quit: irc.renjuan.org (juan@acm.org)) |
2025-08-08 14:55:04 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 260 seconds) |
2025-08-08 14:52:38 +0200 | davidlbowman | (~dlb@user/davidlbowman) davidlbowman |
2025-08-08 14:50:55 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) wootehfoot |
2025-08-08 14:48:51 +0200 | weary-traveler | (~user@user/user363627) user363627 |
2025-08-08 14:48:16 +0200 | AlexNoo | (~AlexNoo@178.34.162.188) (Quit: Leaving) |
2025-08-08 14:47:36 +0200 | AlexZenon | (~alzenon@178.34.162.188) (Quit: ;-) |
2025-08-08 14:45:09 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
2025-08-08 14:44:09 +0200 | euandreh | (~Thunderbi@2804:d59:892b:6600:cfc9:47d1:96e8:b32d) euandreh |
2025-08-08 14:43:36 +0200 | xff0x | (~xff0x@2405:6580:b080:900:3038:cd69:f604:d295) |
2025-08-08 14:40:54 +0200 | Lycurgus | (~juan@user/Lycurgus) Lycurgus |
2025-08-08 14:31:36 +0200 | trickard_ | trickard |
2025-08-08 14:30:25 +0200 | fp | (~Thunderbi@89-27-10-140.bb.dnainternet.fi) fp |
2025-08-08 14:30:08 +0200 | fp | (~Thunderbi@89-27-10-140.bb.dnainternet.fi) (Quit: fp) |
2025-08-08 14:29:32 +0200 | end | (~end@user/end/x-0094621) end^ |
2025-08-08 14:24:41 +0200 | <kuribas> | However I could prove that for every monotype b, if "x : forall a. e", then "x : e[b/a]". In that case a substitution error would give a contradiction, if "a -> b" must work with distinc types, it would fail if substution makes them equal. |
2025-08-08 14:24:22 +0200 | bcksl | (~bcksl@user/bcksl) bcksl |
2025-08-08 14:13:02 +0200 | ljdarj1 | ljdarj |
2025-08-08 14:13:02 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
2025-08-08 14:10:21 +0200 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
2025-08-08 14:06:11 +0200 | <kuribas> | [exa]: So I can make a system, proof it consistent, and have an inference algorithm for that system that I can prove is complete. If I want more garantees, like universal quantification, I'll need more theorems for it. |
2025-08-08 14:05:54 +0200 | end | (~end@user/end/x-0094621) (Quit: end) |
2025-08-08 14:05:53 +0200 | bcksl | (~bcksl@user/bcksl) (Quit: \) |
2025-08-08 14:02:29 +0200 | trickard_ | (~trickard@cpe-49-98-47-163.wireline.com.au) |
2025-08-08 14:02:16 +0200 | trickard | (~trickard@cpe-49-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
2025-08-08 13:59:41 +0200 | poscat | (~poscat@user/poscat) poscat |
2025-08-08 13:59:20 +0200 | poscat | (~poscat@user/poscat) (Remote host closed the connection) |
2025-08-08 13:58:35 +0200 | ttybitnik | (~ttybitnik@user/wolper) ttybitnik |
2025-08-08 13:57:16 +0200 | poscat | (~poscat@user/poscat) poscat |
2025-08-08 13:56:50 +0200 | poscat | (~poscat@user/poscat) (Remote host closed the connection) |
2025-08-08 13:55:15 +0200 | athan | (~athan@syn-047-132-161-157.res.spectrum.com) athan |
2025-08-08 13:52:08 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |