Newest at the top
| 2026-03-12 19:40:27 +0100 | jeremyn | (~jeremy@user/jeremyn) (Quit: Konversation terminated!) |
| 2026-03-12 19:40:10 +0100 | <ski> | it's simultaneously defining two operations, `-' and `?<' such that they together (on the same inputs) are total |
| 2026-03-12 19:40:07 +0100 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-03-12 19:39:41 +0100 | <ski> | Wygulmage : side conditions ? |
| 2026-03-12 19:39:29 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:39:23 +0100 | <ski> | dependently typed version would be `k - m : Fin n | k ?< m : Fin m -| m : Nat , n : Nat , k : Fin (m + n)' |
| 2026-03-12 19:38:45 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:38:42 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:38:02 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:37:38 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:37:37 +0100 | <Wygulmage> | And the side conditions produce type errors if they can't be proven at compile time? |
| 2026-03-12 19:37:06 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:36:46 +0100 | <ski> | no, that's a normal (value-level) `Nat' |
| 2026-03-12 19:36:24 +0100 | <Wygulmage> | ski: So that's using the type-level Nat? |
| 2026-03-12 19:34:39 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-03-12 19:34:09 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:34:04 +0100 | <Wygulmage> | Me a couple hours ago: <Wygulmage> Sorry. Is IRC dead, or did I just come at a bad time? |
| 2026-03-12 19:33:42 +0100 | ski | shrugs |
| 2026-03-12 19:33:25 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:33:22 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:33:17 +0100 | Googulator38 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) |
| 2026-03-12 19:33:16 +0100 | Googulator22 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-03-12 19:33:10 +0100 | someb | (~someb@24.42.43.79) () |
| 2026-03-12 19:32:42 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:32:18 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:31:56 +0100 | <ski> | someb : don't ask to ask, just ask |
| 2026-03-12 19:31:46 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:31:41 +0100 | wbrawner | (~wbrawner@129.146.105.153) wbrawner |
| 2026-03-12 19:31:40 +0100 | <ski> | Wygulmage : the version i showed above |
| 2026-03-12 19:31:02 +0100 | <someb> | anyone online? |
| 2026-03-12 19:30:57 +0100 | <someb> | hello? |
| 2026-03-12 19:30:39 +0100 | someb | (~someb@24.42.43.79) |
| 2026-03-12 19:29:55 +0100 | <Wygulmage> | (I'm reading up on Brzozowski derivatives and quotients of formal languages.) |
| 2026-03-12 19:29:45 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 19:29:15 +0100 | <Wygulmage> | What would a non-dependently typed version look like? |
| 2026-03-12 19:28:49 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:28:05 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:28:02 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:27:22 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:26:58 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:26:26 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:24:48 +0100 | <ski> | (well, the version i was pondering was dependently typed, but you could also have non-dependently typed versions) |
| 2026-03-12 19:24:23 +0100 | <ski> | .. in my imagined functional language, from a while ago, you can write stuff like `m - n : Nat | m ?< n : () -| m : Nat , n : Nat', where either `m - n' or `m ?< n' is well-defined |
| 2026-03-12 19:23:54 +0100 | Googulator53 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-03-12 19:23:31 +0100 | Googulator22 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) |
| 2026-03-12 19:23:29 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:22:45 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:22:42 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:22:02 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:21:38 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |