2025/11/30

Newest at the top

2025-11-30 20:55:32 +0100 <[exa]> hololeap: tbh I was thinking about that very informally too. Usually turns out the SOened can't ever exist if the thing wasn't opened in the first place (unless people are cheating with unsafeCreateWitness or whatever)
2025-11-30 20:55:05 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 244 seconds)
2025-11-30 20:54:36 +0100tomboy64(~tomboy64@user/tomboy64) (Ping timeout: 252 seconds)
2025-11-30 20:54:29 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-11-30 20:53:30 +0100 <hololeap> is there a proper definition somewhere?
2025-11-30 20:53:11 +0100 <lambdabot> parse error (possibly incorrect indentation or mismatched brackets)
2025-11-30 20:53:11 +0100 <lambdabot> <hint>:1:61: error:
2025-11-30 20:53:09 +0100 <hololeap> > We say that SOpened is a runtime witness to s being 'Opened.
2025-11-30 20:53:03 +0100 <hololeap> https://blog.jle.im/entry/introduction-to-singletons-1.html
2025-11-30 20:52:57 +0100 <hololeap> I just realized that I don't exactly know what a "witness" is, even though I've intuited it, more or less
2025-11-30 20:48:16 +0100cephei8(b8652603d7@user/cephei8) cephei8
2025-11-30 20:48:16 +0100cephei8(b8652603d7@2a03:6000:1812:100::1535) (Changing host)
2025-11-30 20:47:48 +0100carbolymer(~carbolyme@delirium.systems) carbolymer
2025-11-30 20:47:33 +0100carbolymer(~carbolyme@delirium.systems) ()
2025-11-30 20:43:52 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds)
2025-11-30 20:39:06 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-11-30 20:32:25 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2025-11-30 20:31:17 +0100FANTOM(~fantom@212.228.181.156)
2025-11-30 20:29:22 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 246 seconds)
2025-11-30 20:27:37 +0100ft(~ft@p508db844.dip0.t-ipconnect.de) ft
2025-11-30 20:26:26 +0100weary-traveler(~user@user/user363627) user363627
2025-11-30 20:26:16 +0100monochrmmonochrom
2025-11-30 20:26:15 +0100monochrom(trebla@216.138.220.146) (Ping timeout: 240 seconds)
2025-11-30 20:26:01 +0100weary-traveler(~user@user/user363627) (Remote host closed the connection)
2025-11-30 20:25:56 +0100FANTOM(~fantom@212.228.181.156) (Ping timeout: 240 seconds)
2025-11-30 20:25:35 +0100ft(~ft@p508db844.dip0.t-ipconnect.de) (Ping timeout: 240 seconds)
2025-11-30 20:24:57 +0100monochrm(trebla@216.138.220.146)
2025-11-30 20:24:26 +0100L29Ah(~L29Ah@wikipedia/L29Ah) L29Ah
2025-11-30 20:21:42 +0100karenw(~karenw@user/karenw) karenw
2025-11-30 20:21:35 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
2025-11-30 20:17:02 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-11-30 20:11:53 +0100samhh_(7569f027cf@2a03:6000:1812:100::e4) samhh
2025-11-30 20:10:22 +0100akspecs(00cc8321af@sourcehut/user/akspecs) akspecs
2025-11-30 20:10:15 +0100whereiseveryone(206ba86c98@2a03:6000:1812:100::2e4) jgart
2025-11-30 20:10:06 +0100alethkit(23bd17ddc6@sourcehut/user/alethkit) alethkit
2025-11-30 20:10:05 +0100probie(cc0b34050a@user/probie) probie
2025-11-30 20:10:02 +0100lucyy(228ee8f0ce@user/lucyy) lucyy
2025-11-30 20:10:02 +0100Ankhers(e99e97ef8e@2a03:6000:1812:100::2a2) Ankhers
2025-11-30 20:10:01 +0100duncan(c6181279e3@user/meow/duncan) duncan
2025-11-30 20:10:00 +0100slondr(cf9f9e8f44@2a03:6000:1812:100::10b6) slondr
2025-11-30 20:09:58 +0100sm2n(ae95cb1267@user/sm2n) sm2n
2025-11-30 20:09:58 +0100rselim(ce261f06ff@user/milesrout) milesrout
2025-11-30 20:09:58 +0100samhh(7569f027cf@2a03:6000:1812:100::e4) samhh
2025-11-30 20:09:57 +0100simendsjo(34b0550437@2a03:6000:1812:100::1441) simendsjo
2025-11-30 20:09:57 +0100shreyasminocha(51fdc93eda@user/shreyasminocha) shreyasminocha
2025-11-30 20:09:57 +0100JoelMcCracken(5ea8252fbb@2a03:6000:1812:100::10e3) JoelMcCracken
2025-11-30 20:09:57 +0100septimi(9f60f4cb70@user/septimi) septimi
2025-11-30 20:09:55 +0100RussetParrotBear(45ce440a48@2a03:6000:1812:100::e2)
2025-11-30 20:09:52 +0100cpli(77fc530071@2a03:6000:1812:100::252) cpli
2025-11-30 20:09:45 +0100ursa-major(114efe6c39@2a03:6000:1812:100::11f3) ursa-major