Newest at the top
2024-10-07 15:40:57 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
2024-10-07 15:40:13 +0200 | youthlic | (~Thunderbi@user/youthlic) youthlic |
2024-10-07 15:40:11 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3313-f515-191c-fe44-fc95-fb26.rev.sfr.net) alexherbo2 |
2024-10-07 15:39:52 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3313-f515-191c-fe44-fc95-fb26.rev.sfr.net) (Remote host closed the connection) |
2024-10-07 15:37:34 +0200 | youthlic | (~Thunderbi@user/youthlic) (Remote host closed the connection) |
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 |