Newest at the top
| 2025-03-21 17:23:25 +0100 | notdabs | (~Owner@2600:1700:69cf:9000:314f:c6fc:a776:72e4) |
| 2025-03-21 17:23:06 +0100 | <haskellbridge> | <Bowuigi> How are those useful? I mean, order dependency is nice but do they make something more elegant? |
| 2025-03-21 17:23:03 +0100 | notdabs | (~Owner@2600:1700:69cf:9000:314f:c6fc:a776:72e4) (Remote host closed the connection) |
| 2025-03-21 17:11:20 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-03-21 17:07:55 +0100 | Square | (~Square@user/square) Square |
| 2025-03-21 17:07:55 +0100 | euleritian | (~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de) (Ping timeout: 244 seconds) |
| 2025-03-21 17:06:58 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-03-21 17:05:51 +0100 | <EvanR> | so x doesn't equal x because equal doesn't exist |
| 2025-03-21 17:04:57 +0100 | <EvanR> | (yet) |
| 2025-03-21 17:04:31 +0100 | <EvanR> | I actually veered off, the presets are "sets" without equality among the elements |
| 2025-03-21 17:03:29 +0100 | <roconnor> | I though they were setoids without reflexivity. |
| 2025-03-21 17:03:14 +0100 | <roconnor> | Oh I misunderstood what your presets were. |
| 2025-03-21 17:01:17 +0100 | <EvanR> | yes? |
| 2025-03-21 17:00:29 +0100 | <roconnor> | EvanR: PERs: Partial Equivalence Relations |
| 2025-03-21 16:55:39 +0100 | vpan | (~vpan@212.117.1.172) |
| 2025-03-21 16:51:18 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2025-03-21 16:50:52 +0100 | euleritian | (~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de) |
| 2025-03-21 16:50:26 +0100 | wildsalander | (~wildsalan@81-175-155-97.bb.dnainternet.fi) (Ping timeout: 252 seconds) |
| 2025-03-21 16:50:04 +0100 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-03-21 16:45:40 +0100 | wildsalander | (~wildsalan@81-175-155-97.bb.dnainternet.fi) |
| 2025-03-21 16:43:39 +0100 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 2025-03-21 16:43:13 +0100 | euleritian | (~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-03-21 16:42:54 +0100 | <EvanR> | ok I got confused, = is the relation being defined |
| 2025-03-21 16:41:51 +0100 | jespada | (~jespada@2800:a4:228e:4800:8c77:166d:4542:2a56) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-03-21 16:41:13 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2025-03-21 16:40:22 +0100 | wildsalander | (~wildsalan@81-175-155-97.bb.dnainternet.fi) (Ping timeout: 268 seconds) |
| 2025-03-21 16:38:41 +0100 | <EvanR> | (and other properties but, they also involve "=") |
| 2025-03-21 16:38:11 +0100 | <EvanR> | xD |
| 2025-03-21 16:37:28 +0100 | <EvanR> | was just reading about "presets" which are setoids (a set that comes equipped with an equivalence relation) without the equivalence relation provided. And then it explained "a preset becomes a set if you give it a relation which.... is reflexive (x = x)" |
| 2025-03-21 16:37:14 +0100 | <tomsmeding> | also not particularly efficient. |
| 2025-03-21 16:36:10 +0100 | <absence> | Proving things with singletons sounds like it will quickly escalate into "not worth it". :p |
| 2025-03-21 16:34:24 +0100 | <tomsmeding> | we're in #haskell, not in #agda ;) |
| 2025-03-21 16:34:04 +0100 | <EvanR> | type O |
| 2025-03-21 16:34:00 +0100 | <EvanR> | er |
| 2025-03-21 16:33:58 +0100 | <EvanR> | oh was reading : as "type off" |
| 2025-03-21 16:33:57 +0100 | <tomsmeding> | seems so |
| 2025-03-21 16:33:55 +0100 | <lambdabot> | True |
| 2025-03-21 16:33:54 +0100 | <tomsmeding> | > x == x |
| 2025-03-21 16:33:35 +0100 | <EvanR> | x = x ? |
| 2025-03-21 16:33:18 +0100 | <tomsmeding> | Now, even the implication `Subset a b => Subset (x:a) (x:b)` is not directly inferrable from the given instances, but you could prove it perhaps, given singletons for those lists |
| 2025-03-21 16:32:49 +0100 | <absence> | Oh right, that makes sense. |
| 2025-03-21 16:32:01 +0100 | <tomsmeding> | [1,1] is a subset of [1,2], but [1] is not a subset of [2] |
| 2025-03-21 16:31:36 +0100 | <tomsmeding> | absence: sure, Subset a b implies Subset (x:a) (x:b). But the other way round does not hold |
| 2025-03-21 16:31:12 +0100 | <absence> | I'm not sure I see how adding an x to both of them breaks the subset relationship... |
| 2025-03-21 16:30:27 +0100 | as___ | (~as@2800:a4:396:c900:c2ca:9624:369a:7d24) (Ping timeout: 265 seconds) |
| 2025-03-21 16:28:31 +0100 | berzerk | (~berzerk@2800:a4:396:c900:c2ca:9624:369a:7d24) (Ping timeout: 265 seconds) |
| 2025-03-21 16:26:47 +0100 | aristid | (sid1599@id-1599.uxbridge.irccloud.com) |
| 2025-03-21 16:25:56 +0100 | jackdk | (sid373013@cssa/jackdk) jackdk |
| 2025-03-21 16:25:08 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-03-21 16:24:44 +0100 | <tomsmeding> | that |