Newest at the top
| 2024-10-08 00:24:21 +0200 | mantraofpie | (~mantraofp@user/mantraofpie) (Ping timeout: 260 seconds) |
| 2024-10-08 00:12:22 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) raehik |
| 2024-10-08 00:09:12 +0200 | andrewboltachev | (~andrey@178.141.123.3) (Quit: Leaving.) |
| 2024-10-08 00:04:00 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2024-10-08 00:02:58 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-10-08 00:00:11 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-10-07 23:59:54 +0200 | euleritian | (~euleritia@dynamic-176-006-132-124.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-10-07 23:59:41 +0200 | Guest82 | (~Guest82@152.44.49.129) (Client Quit) |
| 2024-10-07 23:58:41 +0200 | Guest82 | (~Guest82@152.44.49.129) |
| 2024-10-07 23:54:25 +0200 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2024-10-07 23:51:57 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 2024-10-07 23:40:26 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2024-10-07 23:40:12 +0200 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2024-10-07 23:37:35 +0200 | supercode | (~supercode@user/supercode) supercode |
| 2024-10-07 23:34:30 +0200 | bliminse | (~bliminse@user/bliminse) bliminse |
| 2024-10-07 23:33:00 +0200 | <yin> | i don't think tgis would be a good thing for Haskell to have. i was just curious of the implications |
| 2024-10-07 23:32:19 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2024-10-07 23:29:28 +0200 | sourcetarius | (~sourcetar@user/sourcetarius) sourcetarius |
| 2024-10-07 23:12:44 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2024-10-07 23:08:20 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 252 seconds) |
| 2024-10-07 23:04:04 +0200 | CiaoSen | (~Jura@2a05:5800:2e4:9e00:ca4b:d6ff:fec1:99da) (Ping timeout: 260 seconds) |
| 2024-10-07 22:50:53 +0200 | michalz | (~michalz@185.246.207.217) (Remote host closed the connection) |
| 2024-10-07 22:36:39 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2024-10-07 22:36:29 +0200 | <dolio> | Oh, nice. |
| 2024-10-07 22:35:57 +0200 | <dolio> | Is that too new for readthedocs? |
| 2024-10-07 22:35:57 +0200 | <ncf> | https://agda.readthedocs.io/en/latest/language/with-abstraction.html#left-hand-side-let-bindings |
| 2024-10-07 22:35:48 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2024-10-07 22:35:42 +0200 | <monochrom> | Yikes haha that sounds like syntax inflation. |
| 2024-10-07 22:35:29 +0200 | ljdarj1 | (~Thunderbi@user/ljdarj) (Remote host closed the connection) |
| 2024-10-07 22:35:22 +0200 | <ncf> | they've added "using" or whatever recently |
| 2024-10-07 22:34:39 +0200 | LukeHoersten | (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-10-07 22:33:51 +0200 | <dolio> | Agda has an analogous annoyance. Sometimes I'd like to define something in a `where` that I use in a `with`. But I can't do that, because the `with` introduces clauses that each have their own `where`, not vice versa. |
| 2024-10-07 22:33:47 +0200 | <monochrom> | in fact, also available to the guard conditions. "case x:xt | z > 0 -> ... where z=x+2" is OK. |
| 2024-10-07 22:33:34 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 260 seconds) |
| 2024-10-07 22:32:58 +0200 | <monochrom> | "case x:xt | x > 0 -> y | otherwise -> - y where y = x*x" y is available to both branches. |
| 2024-10-07 22:31:37 +0200 | <monochrom> | Yes that one is right. |
| 2024-10-07 22:31:36 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-10-07 22:30:54 +0200 | <dolio> | E.G. definitions in a `where` are in scope in guards, I think, which would not be possible if the `where` were part of the expression after the guards. |
| 2024-10-07 22:30:49 +0200 | <monochrom> | This is why "let x = 0:y in x where y = 1:x" is the best of both worlds. >:) |
| 2024-10-07 22:30:45 +0200 | CiaoSen | (~Jura@2a05:5800:2e4:9e00:ca4b:d6ff:fec1:99da) CiaoSen |
| 2024-10-07 22:30:40 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2024-10-07 22:30:22 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-10-07 22:30:15 +0200 | bliminse | (~bliminse@user/bliminse) (Quit: leaving) |
| 2024-10-07 22:29:57 +0200 | <monochrom> | The dilemma between "defining stuff out of the blue before getting to the point" and "the point using terms out of the blue before being defined" >:) |
| 2024-10-07 22:29:47 +0200 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2024-10-07 22:29:43 +0200 | <dolio> | Also, making where an expression like Landin has its disadvantages w/r/t how Haskell's syntax currently works. |
| 2024-10-07 22:27:51 +0200 | <dolio> | I think having `where` reference things in other scopes based on the occurrence of the bound names sounds pretty confusing and difficult to figure out. |
| 2024-10-07 22:23:48 +0200 | <EvanR> | like a damn math book, they define stuff seemingly out of blue before getting to the point |
| 2024-10-07 22:23:28 +0200 | <EvanR> | where the definitions are in order |
| 2024-10-07 22:23:08 +0200 | <EvanR> | I'm finding where clause to be awkward sometimes. Unless it's a wild mess of definitions that must be necessarily out of order, or there's no logical order of presentation, I've been liking block of let bindings ending with an in |