2024/05/18

Newest at the top

2024-05-18 23:14:09 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-05-18 23:07:20 +0200zetef(~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f) (Ping timeout: 260 seconds)
2024-05-18 23:04:00 +0200petrichor(~znc-user@user/petrichor) (Quit: ZNC 1.8.2 - https://znc.in)
2024-05-18 22:56:02 +0200gmg(~user@user/gehmehgeh) (Ping timeout: 260 seconds)
2024-05-18 22:52:04 +0200zetef(~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f)
2024-05-18 22:50:40 +0200qqq(~qqq@92.43.167.61) (Remote host closed the connection)
2024-05-18 22:47:16 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 260 seconds)
2024-05-18 22:46:51 +0200sawilagar(~sawilagar@user/sawilagar)
2024-05-18 22:46:30 +0200RedFlamingos(~RedFlamin@user/RedFlamingos)
2024-05-18 22:43:28 +0200gmg(~user@user/gehmehgeh)
2024-05-18 22:35:30 +0200gmg(~user@user/gehmehgeh) (Ping timeout: 260 seconds)
2024-05-18 22:34:50 +0200takuan(~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection)
2024-05-18 22:29:30 +0200euleritian(~euleritia@p200300d40f4af8005abbe7e2e78f892d.dip0.t-ipconnect.de)
2024-05-18 22:29:18 +0200euleritian(~euleritia@dynamic-176-006-188-140.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2024-05-18 22:28:52 +0200bionade24(~quassel@2a03:4000:33:45b::1)
2024-05-18 22:28:45 +0200gmg(~user@user/gehmehgeh)
2024-05-18 22:28:38 +0200bionade24(~quassel@2a03:4000:33:45b::1) (Quit: Apocalypse Incoming!)
2024-05-18 22:27:39 +0200fizbin__(~fizbin@user/fizbin)
2024-05-18 22:27:35 +0200pavonia(~user@user/siracusa)
2024-05-18 22:24:44 +0200 <monochrom> >:)
2024-05-18 22:24:13 +0200euleritian(~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 +0200euleritian(~euleritia@p200300d40f4af8006c29977101d489e2.dip0.t-ipconnect.de) (Ping timeout: 240 seconds)
2024-05-18 22:21:36 +0200phma(~phma@2001:5b0:210d:fcc8:b4c9:7a8c:a02a:3e86)
2024-05-18 22:20:44 +0200phma(~phma@host-67-44-208-141.hnremote.net) (Read error: Connection reset by peer)
2024-05-18 22:20:30 +0200chiselfuse(~chiselfus@user/chiselfuse)
2024-05-18 22:19:29 +0200chiselfuse(~chiselfus@user/chiselfuse) (Remote host closed the connection)
2024-05-18 22:14:04 +0200y04nn(~username@2a03:1b20:8:f011::e10d)
2024-05-18 22:13:11 +0200Square(~Square@user/square) (Ping timeout: 264 seconds)
2024-05-18 22:11:06 +0200Pixi(~Pixi@user/pixi)
2024-05-18 22:10:32 +0200Pixi__(~Pixi@user/pixi) (Quit: Leaving)
2024-05-18 22:00:25 +0200waleee(~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 +0200machinedgod(~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 +0200y04nn(~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...?