Newest at the top
| 2025-01-24 14:18:51 +0100 | <ncf> | no |
| 2025-01-24 14:18:25 +0100 | <kuribas> | ncf: it is with impredicative types enabled? |
| 2025-01-24 14:18:12 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-24 14:16:10 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-01-24 14:02:47 +0100 | iamsleepy | (~weechat@2a01:4f9:3070:feff:a9de:dfff:cd7f:fdcd) iamsleepy |
| 2025-01-24 14:02:23 +0100 | iamsleepy | (~weechat@2a01:4f9:3070:feff:9969:2d95:7b68:eef5) (Read error: Connection reset by peer) |
| 2025-01-24 14:01:07 +0100 | visilii | (~visilii@46.61.242.99) |
| 2025-01-24 13:59:48 +0100 | visilii | (~visilii@46.61.242.99) (Read error: Connection reset by peer) |
| 2025-01-24 13:52:49 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-24 13:52:24 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 2025-01-24 13:46:28 +0100 | jespada | (~jespada@2800:a4:2288:4600:a43e:beb4:c592:b90b) jespada |
| 2025-01-24 13:42:35 +0100 | Googulator | (~Googulato@host-88-132-146-182.prtelecom.hu) |
| 2025-01-24 13:33:54 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 2025-01-24 13:33:10 +0100 | dysthesis | (~dysthesis@user/dysthesis) (Remote host closed the connection) |
| 2025-01-24 13:30:55 +0100 | <ncf> | (∃a. ... a ...) -> r is not |
| 2025-01-24 13:30:51 +0100 | <ncf> | dminuoso: (∃a. ... a ...) is an existential type |
| 2025-01-24 13:29:57 +0100 | <ncf> | forall a. Num a is not a type |
| 2025-01-24 13:29:28 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-24 13:21:37 +0100 | Midjak | (~MarciZ@82.66.147.146) Midjak |
| 2025-01-24 13:10:38 +0100 | <dminuoso> | `(∃a. ... a ...) -> r` however is an existential type and it is isomorphic to `∀ a. (... a ... -> r)` |
| 2025-01-24 13:10:25 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 248 seconds) |
| 2025-01-24 13:04:50 +0100 | V | (~v@ircpuzzles/2022/april/winner/V) V |
| 2025-01-24 13:04:45 +0100 | <dminuoso> | kuribas: That type is not existential. |
| 2025-01-24 13:04:29 +0100 | rvalue- | rvalue |
| 2025-01-24 13:03:55 +0100 | ft | (~ft@p508db1ba.dip0.t-ipconnect.de) ft |
| 2025-01-24 13:01:59 +0100 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-01-24 13:00:49 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 2025-01-24 13:00:15 +0100 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 252 seconds) |
| 2025-01-24 12:59:46 +0100 | rvalue- | (~rvalue@user/rvalue) rvalue |
| 2025-01-24 12:54:25 +0100 | euphores | (~SASL_euph@user/euphores) (Ping timeout: 248 seconds) |
| 2025-01-24 12:53:50 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2025-01-24 12:44:08 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-01-24 12:42:22 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-24 12:41:56 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-01-24 12:41:56 +0100 | <merijn> | Whether I was saying that, that depends very much on what context that syntax is in. And my terminology is a sloppy mess anyway :p |
| 2025-01-24 12:40:41 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) wootehfoot |
| 2025-01-24 12:39:43 +0100 | <kuribas> | merijn: Where you saying (forall a. Num a) is an existential, not a universal? |
| 2025-01-24 12:39:43 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-24 12:34:14 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Remote host closed the connection) |
| 2025-01-24 12:34:14 +0100 | hughjfch1 | (~hughjfche@vmi2417424.contaboserver.net) hughjfchen |
| 2025-01-24 12:33:43 +0100 | hughjfch1 | (~hughjfche@vmi2417424.contaboserver.net) (Quit: WeeChat 4.4.3) |
| 2025-01-24 12:27:55 +0100 | dysthesis | (~dysthesis@user/dysthesis) dysthesis |
| 2025-01-24 12:25:24 +0100 | dysthesis | (~dysthesis@user/dysthesis) (Ping timeout: 264 seconds) |
| 2025-01-24 12:23:45 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-24 12:22:56 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-01-24 12:17:19 +0100 | merijn | (~merijn@62.45.137.128) merijn |
| 2025-01-24 12:10:57 +0100 | dysthesis | (~dysthesis@user/dysthesis) dysthesis |
| 2025-01-24 12:08:49 +0100 | Square2 | (~Square4@user/square) Square |
| 2025-01-24 12:07:22 +0100 | xff0x | (~xff0x@2405:6580:b080:900:2b3c:b3c3:f979:5337) |
| 2025-01-24 12:06:50 +0100 | homo | (~homo@user/homo) homo |