Newest at the top
2024-05-18 22:43:28 +0200 | gmg | (~user@user/gehmehgeh) |
2024-05-18 22:35:30 +0200 | gmg | (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
2024-05-18 22:34:50 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
2024-05-18 22:29:30 +0200 | euleritian | (~euleritia@p200300d40f4af8005abbe7e2e78f892d.dip0.t-ipconnect.de) |
2024-05-18 22:29:18 +0200 | euleritian | (~euleritia@dynamic-176-006-188-140.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
2024-05-18 22:28:52 +0200 | bionade24 | (~quassel@2a03:4000:33:45b::1) |
2024-05-18 22:28:45 +0200 | gmg | (~user@user/gehmehgeh) |
2024-05-18 22:28:38 +0200 | bionade24 | (~quassel@2a03:4000:33:45b::1) (Quit: Apocalypse Incoming!) |
2024-05-18 22:27:39 +0200 | fizbin__ | (~fizbin@user/fizbin) |
2024-05-18 22:27:35 +0200 | pavonia | (~user@user/siracusa) |
2024-05-18 22:24:44 +0200 | <monochrom> | >:) |
2024-05-18 22:24:13 +0200 | euleritian | (~euleritia@dynamic-176-006-188-140.176.6.pool.telefonica.de) |
2024-05-18 22:24:06 +0200 | <raehik> | geekosaur: turns out I can copy how singletons-base implements singled Natural subtraction, reifying->performing regular subtraction->unsafeCoercing the result |
2024-05-18 22:23:41 +0200 | euleritian | (~euleritia@p200300d40f4af8006c29977101d489e2.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
2024-05-18 22:21:36 +0200 | phma | (~phma@2001:5b0:210d:fcc8:b4c9:7a8c:a02a:3e86) |
2024-05-18 22:20:44 +0200 | phma | (~phma@host-67-44-208-141.hnremote.net) (Read error: Connection reset by peer) |
2024-05-18 22:20:30 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) |
2024-05-18 22:19:29 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
2024-05-18 22:14:04 +0200 | y04nn | (~username@2a03:1b20:8:f011::e10d) |
2024-05-18 22:13:11 +0200 | Square | (~Square@user/square) (Ping timeout: 264 seconds) |
2024-05-18 22:11:06 +0200 | Pixi | (~Pixi@user/pixi) |
2024-05-18 22:10:32 +0200 | Pixi__ | (~Pixi@user/pixi) (Quit: Leaving) |
2024-05-18 22:00:25 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
2024-05-18 22:00:15 +0200 | <raehik> | geekosaur: even with that package I need to provide a proof that n >= 1... bleh |
2024-05-18 21:39:05 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
2024-05-18 21:37:46 +0200 | <Rembane> | I think 0 is the roundest of the hot take primes |
2024-05-18 21:37:12 +0200 | <ncf> | not to be confused with 2, the least-odd prime |
2024-05-18 21:36:48 +0200 | y04nn | (~username@2a03:1b20:8:f011::e10d) (Ping timeout: 260 seconds) |
2024-05-18 21:34:58 +0200 | <monochrom> | hahaha |
2024-05-18 21:34:51 +0200 | <ncf> | 3 is actually the least odd prime |
2024-05-18 21:34:14 +0200 | <monochrom> | Hot take: 3 is the oddest of odd primes. |
2024-05-18 21:34:08 +0200 | <geekosaur> | the decision was made at some point that, rather than teach the typechecker things like that, it should be done with plugins (iirc) |
2024-05-18 21:33:24 +0200 | <geekosaur> | afaik it just adds constraints for obvious things like that |
2024-05-18 21:33:11 +0200 | <geekosaur> | that might be it |
2024-05-18 21:33:07 +0200 | <raehik> | if possible I'd like to know how to do it manually too |
2024-05-18 21:32:52 +0200 | <raehik> | geekosaur: I know of ghc-typelits-knownnat |
2024-05-18 21:29:59 +0200 | <geekosaur> | or its cousin that I can't recall ottomh |
2024-05-18 21:29:25 +0200 | <geekosaur> | yes. try the natnormalise plugin, I think? |
2024-05-18 21:29:00 +0200 | <ncf> | hmm... is this just GHC being bad |
2024-05-18 21:28:55 +0200 | <ncf> | could not deduce KnownNat (n - 1) from KnownNat n |
2024-05-18 21:26:36 +0200 | <raehik> | ncf: yeah I'm thinking withKnownNat and some unsafeCoerce ing...? |
2024-05-18 21:26:36 +0200 | <ncf> | hmm, i guess it's not clear how to proceed from there |
2024-05-18 21:25:19 +0200 | <lambdabot> | Data.Singletons.TypeLits withKnownNat :: Sing n -> (KnownNat n => r) -> r |
2024-05-18 21:25:18 +0200 | <ski> | @hoogle withKnownNat |
2024-05-18 21:24:30 +0200 | <ncf> | raehik: withKnownNat? |
2024-05-18 21:24:27 +0200 | <ski> | (like there's results where all odd primes are treated the same way, but you have to treat two differently. commonly this is, on some level, because there's only one (unique !) congruence class modulo two which doesn't contain zero) |
2024-05-18 21:24:13 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
2024-05-18 21:23:05 +0200 | <ncf> | that's true |
2024-05-18 21:22:37 +0200 | <ski> | ncf : perhaps it would be nicer with commutative monoids .. but the indices had an order given by `Ix' in this case |
2024-05-18 21:21:52 +0200 | <Rembane> | That's a good quote |