2024/05/18

Newest at the top

2024-05-18 23:35:31 +0200 <mauke> huh?
2024-05-18 23:35:21 +0200 <edrx> anyone knows the name of that f?
2024-05-18 23:35:05 +0200zetef(~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f)
2024-05-18 23:35:05 +0200 <edrx> the translation of [0,1] is not immediate, but I guess that I can find if I find how [0,1] is expanded to f 0 1 for a certain f...
2024-05-18 23:34:35 +0200chiselfuse(~chiselfus@user/chiselfuse) (Remote host closed the connection)
2024-05-18 23:34:32 +0200zetef(~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f) (Read error: Connection reset by peer)
2024-05-18 23:34:11 +0200 <edrx> to Lean...
2024-05-18 23:33:59 +0200 <edrx> do a <- [0,1]; b <- [a+1,a+2]; guard (a+b < 4); return (a,b)
2024-05-18 23:33:53 +0200 <edrx> hi all! I am trying to translate my notes on this
2024-05-18 23:32:47 +0200edrx(~Eduardo@179-191-223-123.static.sumicity.net.br)
2024-05-18 23:31:31 +0200zetef(~quassel@2a02:2f00:5202:1200:3fa2:e908:b522:fa2f)
2024-05-18 23:26:03 +0200sord937(~sord937@gateway/tor-sasl/sord937) (Quit: sord937)
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