Newest at the top
| 2026-02-08 22:18:40 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-08 22:18:04 +0100 | emmanuelux | (~em@user/emmanuelux) emmanuelux |
| 2026-02-08 22:14:57 +0100 | fgarcia | (~lei@user/fgarcia) fgarcia |
| 2026-02-08 22:14:51 +0100 | ystael | (~ystael@user/ystael) (Quit: Lost terminal) |
| 2026-02-08 22:09:37 +0100 | fgarcia | (~lei@user/fgarcia) (Quit: Remote host closed the connection) |
| 2026-02-08 22:07:43 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-02-08 22:04:54 +0100 | <yahb2> | <interactive>:7:41: error: [GHC-27958] ; • Expected kind ‘k0’, but ‘Timed’ has kind ‘(k0 -> *) -> *’ ; • In the first argument of ‘a’, namely ‘Timed’ ; In the type ‘(a Timed)’ ; ... |
| 2026-02-08 22:04:54 +0100 | <tomsmeding> | % data Timed a = Later (Timed a) | Now (a Timed) |
| 2026-02-08 22:04:31 +0100 | <chromoblob> | Rembane: no, i doubt it will work because i can see that Timed would have an infinite kind |
| 2026-02-08 22:03:57 +0100 | emmanuelux | (~em@user/emmanuelux) (Read error: Connection reset by peer) |
| 2026-02-08 22:03:56 +0100 | emmanuelux | (~em@user/emmanuelux) emmanuelux |
| 2026-02-08 22:03:55 +0100 | <chromoblob> | something like "data Timed a = Later (Timed a) | Now a" and "data ListTimed a = EmptyTimed | ConsTimed (Timed a) (Timed (ListTimed a))" is intended |
| 2026-02-08 22:03:02 +0100 | <Rembane> | chromoblob: Have you tried them in a Haskell compiler? |
| 2026-02-08 22:02:53 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-08 22:01:31 +0100 | <chromoblob> | tomsmeding: the definitions |
| 2026-02-08 21:56:34 +0100 | emmanuelux | (~em@user/emmanuelux) (Read error: Connection reset by peer) |
| 2026-02-08 21:55:29 +0100 | _JusSx_ | (~username@37.163.117.200) _JusSx_ |
| 2026-02-08 21:55:01 +0100 | divlamir | (~divlamir@user/divlamir) divlamir |
| 2026-02-08 21:54:18 +0100 | _JusSx_ | (~jussx@37.163.117.200) (Quit: leaving) |
| 2026-02-08 21:53:18 +0100 | tomsmeding | is not sure what "this" refers to |
| 2026-02-08 21:52:02 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-02-08 21:47:02 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-08 21:46:49 +0100 | divlamir | (~divlamir@user/divlamir) (Ping timeout: 264 seconds) |
| 2026-02-08 21:45:04 +0100 | emmanuelux | (~em@user/emmanuelux) emmanuelux |
| 2026-02-08 21:41:36 +0100 | emmanuelux | (~em@user/emmanuelux) (Read error: Connection reset by peer) |
| 2026-02-08 21:41:25 +0100 | emmanuelux | (~em@user/emmanuelux) emmanuelux |
| 2026-02-08 21:40:15 +0100 | trickard_ | trickard |
| 2026-02-08 21:38:05 +0100 | emmanuelux | (~em@user/emmanuelux) (Read error: Connection reset by peer) |
| 2026-02-08 21:35:27 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-02-08 21:31:57 +0100 | emmanuelux | (~em@user/emmanuelux) emmanuelux |
| 2026-02-08 21:31:13 +0100 | <L29Ah> | right |
| 2026-02-08 21:30:44 +0100 | bggd_ | (~bgg@2a01:e0a:fd5:f510:7c7b:26be:3fe9:d994) |
| 2026-02-08 21:30:26 +0100 | oats | (~oats@user/oats) oats |
| 2026-02-08 21:30:26 +0100 | <chromoblob> | this can't work, right? |
| 2026-02-08 21:30:24 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-08 21:30:18 +0100 | <chromoblob> | data List1 a t = Empty1 | Cons1 (t a) (t (List1 a)) |
| 2026-02-08 21:30:18 +0100 | <chromoblob> | data Timed a = Later (Timed a) | Now (a Timed) |
| 2026-02-08 21:30:12 +0100 | oats | (~oats@user/oats) (Read error: Connection reset by peer) |
| 2026-02-08 21:28:50 +0100 | emmanuelux | (~em@user/emmanuelux) (Read error: Connection reset by peer) |
| 2026-02-08 21:26:30 +0100 | _JusSx_ | (~jussx@37.163.117.200) |
| 2026-02-08 21:25:13 +0100 | _JusSx_ | (~jussx@37.163.117.200) (Ping timeout: 264 seconds) |
| 2026-02-08 21:23:35 +0100 | emmanuelux | (~em@user/emmanuelux) emmanuelux |
| 2026-02-08 21:19:12 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-02-08 21:18:18 +0100 | Square2 | (~Square@user/square) Square |
| 2026-02-08 21:12:21 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-08 21:09:55 +0100 | emmanuelux | (~em@user/emmanuelux) (Read error: Connection reset by peer) |
| 2026-02-08 21:08:50 +0100 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2026-02-08 21:08:30 +0100 | emmanuelux | (~em@user/emmanuelux) emmanuelux |
| 2026-02-08 21:04:21 +0100 | <mesaoptimizer> | also W40K because "chaos" |
| 2026-02-08 21:03:54 +0100 | <mesaoptimizer> | I read that as concentration camp but I have been thinking about Gentzen a lot lately |