2025/03/30

Newest at the top

2025-03-30 05:03:06 +0200 <haskellbridge> <thirdofmay18081814goya> EvanR: a step is a natural number that designates a pair, given by a natural number and its successor, such that when fed into a function "Nat -> Tree Int", produce a tree that is at most different by a single application of the datatype constructor
2025-03-30 05:02:57 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-03-30 05:02:55 +0200haritz(~hrtz@2a02:8010:65b5:0:5d9a:9bab:ee5e:b737)
2025-03-30 05:02:45 +0200haritz(~hrtz@user/haritz) (Remote host closed the connection)
2025-03-30 05:01:39 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-30 04:59:23 +0200 <EvanR> did I construct let xs = 1 : xs in xs in a finite number of steps, or is it even successfully constructed
2025-03-30 04:58:15 +0200 <monochrom> A step is a finite number of substeps. >:)
2025-03-30 04:57:16 +0200 <EvanR> what's a step
2025-03-30 04:56:57 +0200 <EvanR> thirdofmay18081814goya, "any element of Tree Int can be constructed in a finite number of steps" ...
2025-03-30 04:56:22 +0200j1n37(~j1n37@user/j1n37) (Read error: Connection reset by peer)
2025-03-30 04:50:46 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-03-30 04:43:52 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-30 04:37:48 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-03-30 04:35:13 +0200euphores(~SASL_euph@user/euphores) euphores
2025-03-30 04:33:55 +0200j1n37(~j1n37@user/j1n37) (Read error: Connection reset by peer)
2025-03-30 04:33:22 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds)
2025-03-30 04:28:43 +0200euphores(~SASL_euph@user/euphores) (Ping timeout: 245 seconds)
2025-03-30 04:27:48 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-30 04:15:13 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-03-30 04:15:08 +0200 <EvanR> I will gratefully deposit 0x$1.00 ($2.56) to the account of the first person who finds and reports anything that remains technically, historically, typographically, or politically incorrect. -- knuth
2025-03-30 04:13:30 +0200JuanDaugherty(~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org))
2025-03-30 04:13:11 +0200 <JuanDaugherty> (and credit where credit due to Conway)
2025-03-30 04:12:51 +0200 <JuanDaugherty> https://en.wikipedia.org/wiki/Surreal_number confirmed
2025-03-30 04:11:44 +0200 <JuanDaugherty> issat knuth's?
2025-03-30 04:07:23 +0200 <EvanR> data Surreal = Cut (Tree Surreal) (Tree Surreal)
2025-03-30 04:05:47 +0200roconnor(~quassel@rocq/roconnor) roconnor
2025-03-30 04:05:35 +0200op_4(~tslil@user/op-4/x-9116473) op_4
2025-03-30 04:05:15 +0200roconnor(~quassel@rocq/roconnor) (Ping timeout: 252 seconds)
2025-03-30 04:05:04 +0200op_4(~tslil@user/op-4/x-9116473) (Remote host closed the connection)
2025-03-30 04:02:18 +0200 <EvanR> data Real = Rat Rat | Lim (Rat -> Real)
2025-03-30 04:01:46 +0200 <geekosaur> I was going to say you got that backwards, but in hindsight I guess it depends on how you interpret that name
2025-03-30 04:00:40 +0200 <EvanR> data Rat = Over { numer :: Int, denomMinusOne :: Nat }
2025-03-30 03:59:51 +0200ChaiTRex(~ChaiTRex@user/chaitrex) ChaiTRex
2025-03-30 03:56:36 +0200L29Ah(~L29Ah@wikipedia/L29Ah) (Read error: Connection timed out)
2025-03-30 03:52:58 +0200acidjnk(~acidjnk@p200300d6e71c4f5684d81f92e812b9d0.dip0.t-ipconnect.de) (Ping timeout: 272 seconds)
2025-03-30 03:51:53 +0200tremon(~tremon@83.80.159.219) (Quit: getting boxed in)
2025-03-30 03:51:50 +0200ChaiTRex(~ChaiTRex@user/chaitrex) (Quit: ChaiTRex)
2025-03-30 03:50:48 +0200 <EvanR> data Int = Nat :- Nat
2025-03-30 03:49:10 +0200 <haskellbridge> <thirdofmay18081814goya> right
2025-03-30 03:49:03 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
2025-03-30 03:49:01 +0200 <EvanR> ignoring bottoms
2025-03-30 03:48:18 +0200 <EvanR> thirdofmay18081814goya, data Nat = Z | S !Nat
2025-03-30 03:47:08 +0200roconnor(~quassel@rocq/roconnor) roconnor
2025-03-30 03:46:27 +0200roconnor(~quassel@rocq/roconnor) (Ping timeout: 246 seconds)
2025-03-30 03:38:24 +0200toby-bro(~toby-bro@user/toby-bro) (Ping timeout: 272 seconds)
2025-03-30 03:32:58 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds)
2025-03-30 03:26:51 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds)
2025-03-30 03:25:46 +0200 <haskellbridge> <jv> 'd
2025-03-30 03:21:35 +0200harveypwca(~harveypwc@2601:246:d080:f6e0:27d6:8cc7:eca9:c46c)
2025-03-30 03:18:01 +0200ChaiTRex(~ChaiTRex@user/chaitrex) ChaiTRex