Newest at the top
2024-05-18 23:14:09 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2024-05-18 23:07:20 +0200 | zetef | (~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f) (Ping timeout: 260 seconds) |
2024-05-18 23:04:00 +0200 | petrichor | (~znc-user@user/petrichor) (Quit: ZNC 1.8.2 - https://znc.in) |
2024-05-18 22:56:02 +0200 | gmg | (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
2024-05-18 22:52:04 +0200 | zetef | (~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f) |
2024-05-18 22:50:40 +0200 | qqq | (~qqq@92.43.167.61) (Remote host closed the connection) |
2024-05-18 22:47:16 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 260 seconds) |
2024-05-18 22:46:51 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
2024-05-18 22:46:30 +0200 | RedFlamingos | (~RedFlamin@user/RedFlamingos) |
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...? |