2024/05/18

Newest at the top

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...?
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 +0200L29Ah(~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