Newest at the top
| 2024-05-18 04:50:35 +0200 | cheater_ | (~Username@user/cheater) |
| 2024-05-18 04:49:33 +0200 | <talismanick> | I guess it's natural for typeclass law proofs to be impervious to intuition because metaproofs are apt to be like that? |
| 2024-05-18 04:44:03 +0200 | Axman6 | (~Axman6@user/axman6) (Ping timeout: 264 seconds) |
| 2024-05-18 04:41:03 +0200 | <talismanick> | exercise* |
| 2024-05-18 04:40:52 +0200 | <talismanick> | if types are propositions and programs are proofs, then mechanically the Monad instance for State is certainly an excersive in understanding through proof - it's basically dataflow through let-binding, as I see it |
| 2024-05-18 04:28:40 +0200 | bwe | (~bwe@2a01:4f8:1c1c:4878::2) |
| 2024-05-18 04:28:32 +0200 | mesaoptimizer | (~mesaoptim@user/PapuaHardyNet) (Ping timeout: 268 seconds) |
| 2024-05-18 04:28:32 +0200 | bwe | (~bwe@2a01:4f8:1c1c:4878::2) (Ping timeout: 268 seconds) |
| 2024-05-18 04:24:31 +0200 | kimiamania | (~76637481@user/kimiamania) |
| 2024-05-18 04:24:08 +0200 | kimiamania | (~76637481@user/kimiamania) (Quit: Ping timeout (120 seconds)) |
| 2024-05-18 04:23:32 +0200 | ringo___ | (~ringo@157.230.117.128) |
| 2024-05-18 04:22:34 +0200 | Athas | (athas@2a01:7c8:aaac:1cf:3ae1:f43a:30e:d1d8) |
| 2024-05-18 04:22:22 +0200 | Athas | (athas@sigkill.dk) (Ping timeout: 268 seconds) |
| 2024-05-18 04:21:45 +0200 | ringo___ | (~ringo@157.230.117.128) (Ping timeout: 268 seconds) |
| 2024-05-18 04:18:03 +0200 | cjb | (~cjb@user/cjb) |
| 2024-05-18 04:14:16 +0200 | tcard | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 2024-05-18 04:12:28 +0200 | tcard | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Quit: Leaving) |
| 2024-05-18 04:11:28 +0200 | td_ | (~td@i53870939.versanet.de) |
| 2024-05-18 04:09:34 +0200 | td_ | (~td@i53870915.versanet.de) (Ping timeout: 246 seconds) |
| 2024-05-18 04:05:57 +0200 | dyniec | (~dyniec@dybiec.info) (Quit: WeeChat 4.1.1) |
| 2024-05-18 04:05:43 +0200 | m257 | (~maaz@bras-base-hspron0502w-grc-15-174-92-92-146.dsl.bell.ca) |
| 2024-05-18 04:00:50 +0200 | fliife | (~fliife@user/fliife) |
| 2024-05-18 04:00:02 +0200 | fliife | (~fliife@user/fliife) (Quit: ZNC 1.8.2+deb2build5 - https://znc.in) |
| 2024-05-18 03:40:46 +0200 | Ranhir | (~Ranhir@157.97.53.139) |
| 2024-05-18 03:35:59 +0200 | addfb3 | (~dante@user/addfb3) (Ping timeout: 256 seconds) |
| 2024-05-18 03:15:40 +0200 | joeyadams | (~joeyadams@2603:6010:5100:2ed:cfe3:13e2:96f6:9d2c) (Quit: Leaving) |
| 2024-05-18 03:14:37 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 246 seconds) |
| 2024-05-18 03:14:35 +0200 | Ranhir | (~Ranhir@157.97.53.139) (Quit: KVIrc 5.0.0 Aria http://www.kvirc.net/) |
| 2024-05-18 03:08:24 +0200 | otto_s | (~user@p5b044b71.dip0.t-ipconnect.de) |
| 2024-05-18 03:06:34 +0200 | otto_s | (~user@p5b0448c7.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 2024-05-18 02:58:35 +0200 | y04nn | (~username@2a03:1b20:8:f011::e10d) (Ping timeout: 256 seconds) |
| 2024-05-18 02:49:47 +0200 | m257 | (~maaz@bras-base-hspron0502w-grc-15-174-92-92-146.dsl.bell.ca) (Ping timeout: 252 seconds) |
| 2024-05-18 02:14:50 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2024-05-18 02:13:18 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 260 seconds) |
| 2024-05-18 02:00:25 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
| 2024-05-18 01:55:43 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2024-05-18 01:54:55 +0200 | internatetional | (~nate@2001:448a:20a3:c2e5:9ba2:a48e:b934:7d97) (Quit: WeeChat 4.2.2) |
| 2024-05-18 01:42:17 +0200 | <ski> | presumably understanding is objective insofar as it allows someone to better predict, diagnose, design |
| 2024-05-18 01:40:31 +0200 | Lycurgus | (~georg@user/Lycurgus) (Quit: leaving) |
| 2024-05-18 01:40:05 +0200 | <Hecate> | tomsmeding: eyo, do you want a PR to enable linear-base for GHC 9.10 on the playground? |
| 2024-05-18 01:27:00 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-05-18 01:26:05 +0200 | <Lycurgus> | without qualification that is; demonstrated understanding brings you back |
| 2024-05-18 01:25:08 +0200 | <Lycurgus> | feel, qualia, obscure thing |
| 2024-05-18 01:24:37 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) |
| 2024-05-18 01:24:24 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) (Read error: Connection reset by peer) |
| 2024-05-18 01:22:41 +0200 | <Lycurgus> | a feel of cognition |
| 2024-05-18 01:21:47 +0200 | <Lycurgus> | 'understanding' - that's a feel innit? |
| 2024-05-18 01:21:31 +0200 | Lycurgus | (~georg@user/Lycurgus) |
| 2024-05-18 01:18:54 +0200 | <dolio> | I've been reading a book with some people, and it seems like most of the proofs are less believable than the facts they state. |
| 2024-05-18 01:17:58 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |