2025/08/08

Newest at the top

2025-08-08 15:58:23 +0200Cale(~cale@2607:fea8:995f:f126:15c3:35a5:81ac:187c) Cale
2025-08-08 15:51:31 +0200smiesner(b0cf5acf8c@user/smiesner) smiesner
2025-08-08 15:51:24 +0200smiesner(b0cf5acf8c@user/smiesner) (Server closed connection)
2025-08-08 15:48:14 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-08-08 15:47:30 +0200jespada(~jespada@2800:a4:2228:2400:e5a0:dd56:e91c:d25b) jespada
2025-08-08 15:39:04 +0200jespada(~jespada@r179-25-146-183.dialup.adsl.anteldata.net.uy) (Quit: Textual IRC Client: www.textualapp.com)
2025-08-08 15:37:59 +0200statusfailed(~statusfai@statusfailed.com) ()
2025-08-08 15:36:54 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-08-08 15:24:17 +0200sprotte24(~sprotte24@p200300d16f43d3003d43dd3d16486e1e.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
2025-08-08 15:23:18 +0200dyniec(~dyniec@dybiec.info)
2025-08-08 15:22:41 +0200dyniec(~dyniec@dybiec.info) (Remote host closed the connection)
2025-08-08 15:22:40 +0200AlexZenon(~alzenon@178.34.162.188)
2025-08-08 15:21:57 +0200Vajb(~Vajb@n4ff0xajgx7huazq3a1-1.v6.elisa-mobile.fi) (Ping timeout: 248 seconds)
2025-08-08 15:21:02 +0200AlexNoo(~AlexNoo@178.34.162.188)
2025-08-08 15:05:35 +0200statusfailed(~statusfai@statusfailed.com) statusfailed
2025-08-08 15:02:58 +0200haritz(~hrtz@user/haritz) haritz
2025-08-08 15:02:58 +0200haritz(~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) (Changing host)
2025-08-08 15:02:58 +0200haritz(~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8)
2025-08-08 15:00:24 +0200Lycurgus(~juan@user/Lycurgus) (Quit: irc.renjuan.org (juan@acm.org))
2025-08-08 14:55:04 +0200CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 260 seconds)
2025-08-08 14:52:38 +0200davidlbowman(~dlb@user/davidlbowman) davidlbowman
2025-08-08 14:50:55 +0200wootehfoot(~wootehfoo@user/wootehfoot) wootehfoot
2025-08-08 14:48:51 +0200weary-traveler(~user@user/user363627) user363627
2025-08-08 14:48:16 +0200AlexNoo(~AlexNoo@178.34.162.188) (Quit: Leaving)
2025-08-08 14:47:36 +0200AlexZenon(~alzenon@178.34.162.188) (Quit: ;-)
2025-08-08 14:45:09 +0200pavonia(~user@user/siracusa) (Quit: Bye!)
2025-08-08 14:44:09 +0200euandreh(~Thunderbi@2804:d59:892b:6600:cfc9:47d1:96e8:b32d) euandreh
2025-08-08 14:43:36 +0200xff0x(~xff0x@2405:6580:b080:900:3038:cd69:f604:d295)
2025-08-08 14:40:54 +0200Lycurgus(~juan@user/Lycurgus) Lycurgus
2025-08-08 14:31:36 +0200trickard_trickard
2025-08-08 14:30:25 +0200fp(~Thunderbi@89-27-10-140.bb.dnainternet.fi) fp
2025-08-08 14:30:08 +0200fp(~Thunderbi@89-27-10-140.bb.dnainternet.fi) (Quit: fp)
2025-08-08 14:29:32 +0200end(~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 +0200bcksl(~bcksl@user/bcksl) bcksl
2025-08-08 14:13:02 +0200ljdarj1ljdarj
2025-08-08 14:13:02 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
2025-08-08 14:10:21 +0200ljdarj1(~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 +0200end(~end@user/end/x-0094621) (Quit: end)
2025-08-08 14:05:53 +0200bcksl(~bcksl@user/bcksl) (Quit: \)
2025-08-08 14:02:29 +0200trickard_(~trickard@cpe-49-98-47-163.wireline.com.au)
2025-08-08 14:02:16 +0200trickard(~trickard@cpe-49-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
2025-08-08 13:59:41 +0200poscat(~poscat@user/poscat) poscat
2025-08-08 13:59:20 +0200poscat(~poscat@user/poscat) (Remote host closed the connection)
2025-08-08 13:58:35 +0200ttybitnik(~ttybitnik@user/wolper) ttybitnik
2025-08-08 13:57:16 +0200poscat(~poscat@user/poscat) poscat
2025-08-08 13:56:50 +0200poscat(~poscat@user/poscat) (Remote host closed the connection)
2025-08-08 13:55:15 +0200athan(~athan@syn-047-132-161-157.res.spectrum.com) athan
2025-08-08 13:52:08 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)