Newest at the top
| 2025-04-28 16:58:49 +0200 | <EvanR> | that's decidedly larger than DBL_DECIMAL_DIG on my computer (17) |
| 2025-04-28 16:57:07 +0200 | <EvanR> | oh |
| 2025-04-28 16:56:38 +0200 | <int-e> | EvanR: so it's due to how that float.exposed website works |
| 2025-04-28 16:55:59 +0200 | <int-e> | (doesn't count leading zeros either) |
| 2025-04-28 16:55:28 +0200 | <lambdabot> | 22 |
| 2025-04-28 16:55:27 +0200 | <int-e> | > length "2.29999995231628417969" |
| 2025-04-28 16:55:10 +0200 | <int-e> | EvanR: this.max_digits = 21 in FloatConfig() in Float.js (doesn't count the decimal point) |
| 2025-04-28 16:54:57 +0200 | <lambdabot> | "2.29999999999999982236431605997495353221893310546875" |
| 2025-04-28 16:54:55 +0200 | <glguy> | > Data.Number.CReal.showCReal 50 (realToFrac 2.3) |
| 2025-04-28 16:54:37 +0200 | son0p | (~ff@2800:e6:4001:f995:7f79:d961:a77:e30d) son0p |
| 2025-04-28 16:53:10 +0200 | <ski> | using existential, or the CPS encoding or data type encoding of that) |
| 2025-04-28 16:53:04 +0200 | <ski> | hm, also with indexed types (similar to GADTs in Haskell), you can recover some (statically) unknown information, by matching on data constructors, this giving you information about the shape of the indices, "reflecting info from run-time back to compile-time by the `case'". this would also work if the value of the indexed data type is generated at run-time (and the indices are erased, perhaps expressed |
| 2025-04-28 16:52:53 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-04-28 16:52:29 +0200 | son0p | (~ff@2800:e6:4001:f995:7f79:d961:a77:e30d) (Ping timeout: 245 seconds) |
| 2025-04-28 16:50:08 +0200 | <ski> | "if we read something from stdin and make a type level Nat from it then can we make arbitrary compile time arithmetic on it?" -- you could read two vectors of non-empty lines, terminated by empty lines, then concatenate those two vectors, have the (statically) unknown length of the resulting vector be known to be the sum of the (statically) unknown lengths of the first two vectors |
| 2025-04-28 16:50:08 +0200 | loonycyborg | (loonycybor@wesnoth/developer/loonycyborg) loonycyborg |
| 2025-04-28 16:47:22 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2025-04-28 16:47:04 +0200 | loonycyborg | (loonycybor@wesnoth/developer/loonycyborg) (Read error: Connection reset by peer) |
| 2025-04-28 16:45:21 +0200 | <EvanR> | with that length |
| 2025-04-28 16:44:57 +0200 | <EvanR> | I wonder where 2.29999995231628417969 comes fro |
| 2025-04-28 16:44:38 +0200 | acidjnk_new | (~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de) acidjnk |
| 2025-04-28 16:42:33 +0200 | son0p | (~ff@2800:e6:4001:f995:7f79:d961:a77:e30d) son0p |
| 2025-04-28 16:42:32 +0200 | <lambdabot> | 229999999999999982236431605997495353221893310546875000 |
| 2025-04-28 16:42:31 +0200 | <int-e> | > truncate $ toRational 2.3 * 10^53 |
| 2025-04-28 16:34:26 +0200 | <EvanR> | 0.1000000000000000055511151231257827021181583404541015625 gotta love the "...6875" and "...5625" at the end proclaiming the arrival of a dyadic fraction |
| 2025-04-28 16:31:45 +0200 | acidjnk_new | (~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 2025-04-28 16:30:33 +0200 | <EvanR> | ok |
| 2025-04-28 16:28:24 +0200 | <EvanR> | still doesn't seem right |
| 2025-04-28 16:27:58 +0200 | <EvanR> | 2.29999999999999982236431605997495353221893310546875 🤯 |
| 2025-04-28 16:24:53 +0200 | son0p | (~ff@2800:e6:4001:f995:7f79:d961:a77:e30d) (Ping timeout: 248 seconds) |
| 2025-04-28 16:23:35 +0200 | <EvanR> | unfortunately lambdabot doesn't have scientific to make the expansion easy |
| 2025-04-28 16:21:35 +0200 | <EvanR> | 2.29999995231628417969 is also not the exact decimal value, which would bit a bit longer but still finite |
| 2025-04-28 16:14:22 +0200 | euleritian | (~euleritia@dynamic-176-006-132-060.176.6.pool.telefonica.de) |
| 2025-04-28 16:12:34 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 244 seconds) |
| 2025-04-28 16:11:28 +0200 | tolgo | (~Thunderbi@199.115.144.130) (Client Quit) |
| 2025-04-28 16:11:16 +0200 | tolgo | (~Thunderbi@199.115.144.130) |
| 2025-04-28 16:07:57 +0200 | LainIwakura | (~LainIwaku@user/LainIwakura) LainIwakura |
| 2025-04-28 16:06:23 +0200 | notdabs | (~Owner@2600:1700:69cf:9000:79ef:6a68:163c:c553) |
| 2025-04-28 16:04:54 +0200 | fp | (~Thunderbi@2001:708:20:1406::10c5) fp |
| 2025-04-28 15:57:09 +0200 | LainIwakura | (~LainIwaku@user/LainIwakura) (Quit: Client closed) |
| 2025-04-28 15:56:11 +0200 | duckworld | (~duckworld@user/duckworld) (*.net *.split) |
| 2025-04-28 15:56:11 +0200 | superbil | (~superbil@114-32-231-70.hinet-ip.hinet.net) (*.net *.split) |
| 2025-04-28 15:56:11 +0200 | Axman6 | (~Axman6@user/axman6) (*.net *.split) |
| 2025-04-28 15:51:51 +0200 | Googulator47 | (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) |
| 2025-04-28 15:51:37 +0200 | Googulator47 | (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-04-28 15:43:17 +0200 | prdak | (~Thunderbi@user/prdak) (Ping timeout: 248 seconds) |
| 2025-04-28 15:43:08 +0200 | Goodbye_Vincent1 | (cyvahl@freakshells.net) (Read error: Connection reset by peer) |
| 2025-04-28 15:42:31 +0200 | fp | (~Thunderbi@2001:708:20:1406::10c5) (Ping timeout: 268 seconds) |
| 2025-04-28 15:40:46 +0200 | Teacup | (~teacup@user/teacup) Teacup |
| 2025-04-28 15:39:10 +0200 | Teacup | (~teacup@user/teacup) (Quit: No Ping reply in 180 seconds.) |