Newest at the top
| 2024-10-07 15:29:59 +0200 | ash3en | (~Thunderbi@89.246.174.164) ash3en |
| 2024-10-07 15:29:37 +0200 | LukeHoersten | (~LukeHoers@user/lukehoersten) LukeHoersten |
| 2024-10-07 15:29:33 +0200 | ash3en | (~Thunderbi@89.246.174.164) (Quit: ash3en) |
| 2024-10-07 15:27:20 +0200 | <Duste3> | Ok thanks |
| 2024-10-07 15:22:52 +0200 | <tomsmeding> | (it's also inconsistent as a theorem prover for a bunch of other reasons) |
| 2024-10-07 15:22:30 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 2024-10-07 15:22:05 +0200 | <tomsmeding> | but do note that Haskell is inconsistent when viewed as a theorem prover, because Type \in Type (where Type is the kind of types that can hold values, sometimes written *) |
| 2024-10-07 15:21:54 +0200 | picnoir | (~picnoir@about/aquilenet/vodoo/NinjaTrappeur) NinjaTrappeur |
| 2024-10-07 15:20:47 +0200 | <tomsmeding> | not sure about the precise numbering of the universe levels, but it indeed corresponds to one universe level higher than types |
| 2024-10-07 15:20:26 +0200 | <tomsmeding> | Duste3: values have types, and types have kinds |
| 2024-10-07 15:20:19 +0200 | picnoir | (~picnoir@about/aquilenet/vodoo/NinjaTrappeur) (Quit: WeeChat 4.4.2) |
| 2024-10-07 15:18:21 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 15:16:42 +0200 | ash3en | (~Thunderbi@89.246.174.164) ash3en |
| 2024-10-07 15:16:36 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
| 2024-10-07 15:14:49 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-10-07 15:13:03 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 276 seconds) |
| 2024-10-07 15:09:11 +0200 | Typedfern | (~Typedfern@124.red-83-37-29.dynamicip.rima-tde.net) |
| 2024-10-07 15:08:30 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Ping timeout: 276 seconds) |
| 2024-10-07 15:07:29 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2024-10-07 15:06:57 +0200 | CiaoSen | (~Jura@2a05:5800:2e4:9e00:ca4b:d6ff:fec1:99da) (Ping timeout: 248 seconds) |
| 2024-10-07 15:06:33 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 15:05:54 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 276 seconds) |
| 2024-10-07 15:03:23 +0200 | <Duste3> | Are Kinds the same thing as Type 1 universe level in a theorem prover like Lean? |
| 2024-10-07 15:03:19 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-10-07 15:01:54 +0200 | Duste3 | (~Duste3@2a0c:5a84:b809:8900:87e9:2b45:1b5f:c816) |
| 2024-10-07 15:01:03 +0200 | cfricke | (~cfricke@user/cfricke) cfricke |
| 2024-10-07 15:00:48 +0200 | cfricke | (~cfricke@user/cfricke) (Remote host closed the connection) |
| 2024-10-07 15:00:40 +0200 | cfricke | (~cfricke@user/cfricke) cfricke |
| 2024-10-07 15:00:34 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 15:00:23 +0200 | cfricke | (~cfricke@user/cfricke) (Remote host closed the connection) |
| 2024-10-07 14:56:49 +0200 | Typedfern | (~Typedfern@124.red-83-37-29.dynamicip.rima-tde.net) (Ping timeout: 265 seconds) |
| 2024-10-07 14:53:42 +0200 | dyniec | (~dyniec@dybiec.info) dyniec |
| 2024-10-07 14:49:29 +0200 | sourcetarius | (~sourcetar@user/sourcetarius) (Quit: sourcetarius) |
| 2024-10-07 14:49:05 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 2024-10-07 14:47:37 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-07 14:47:17 +0200 | <lambdabot> | e + a + b + c + d |
| 2024-10-07 14:47:16 +0200 | <kuribas> | > foldl (+) e [a, b, c, d] |
| 2024-10-07 14:47:08 +0200 | <lambdabot> | a + (b + (c + (d + e))) |
| 2024-10-07 14:47:07 +0200 | <kuribas> | > foldr (+) e [a, b, c, d] |
| 2024-10-07 14:46:54 +0200 | <lambdabot> | • In the third argument of ‘foldr’, namely ‘e’ |
| 2024-10-07 14:46:54 +0200 | <lambdabot> | • Couldn't match expected type ‘t0 [Expr]’ with actual type ‘Expr’ |
| 2024-10-07 14:46:54 +0200 | <lambdabot> | error: |
| 2024-10-07 14:46:53 +0200 | <kuribas> | > foldr (+) [a, b, c, d] e |
| 2024-10-07 14:46:52 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 2024-10-07 14:44:13 +0200 | merijn | (~merijn@77.242.116.146) merijn |
| 2024-10-07 14:42:29 +0200 | comerijn | (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 2024-10-07 14:41:10 +0200 | <Leonard26> | I have a function that gets called every 1s, that's why the variable must change each time |
| 2024-10-07 14:39:46 +0200 | <Leonard26> | I am working with Gstreamer, I have a video stream that needs to fade out, the values I am talking about are the opacity property of the video. |
| 2024-10-07 14:37:53 +0200 | <hc> | tdammers: kk, thanks, that makes sense :-) |
| 2024-10-07 14:36:18 +0200 | <__monty__> | What's your expected output? |