Newest at the top
| 2026-02-07 11:30:21 +0100 | p3n | (~p3n@217.198.124.246) (Quit: ZNC 1.10.1 - https://znc.in) |
| 2026-02-07 11:28:34 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 11:28:16 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) chromoblob\0 |
| 2026-02-07 11:27:06 +0100 | <probie> | I guess you could have have a `make` function which takes various kinds of records as arguments, but in practice that's not ergonomic, and it also deviates heavily from the C API, which is why most of the documentation you'll find online is |
| 2026-02-07 11:26:27 +0100 | <probie> | gentauro: how would you shrink it, short of abbreviating things. You need to convey 4 things; "it's new", "the name can't be anything already generated", "it's an int" and "it's a var"? |
| 2026-02-07 11:25:29 +0100 | AlexNoo__ | (~AlexNoo@85.174.182.86) (Ping timeout: 260 seconds) |
| 2026-02-07 11:25:20 +0100 | <jreicher> | Oh, I think I know what you mean |
| 2026-02-07 11:25:06 +0100 | <jreicher> | gentauro: "Hungarian notation"? |
| 2026-02-07 11:25:03 +0100 | <gentauro> | probie: to verbose (at least for me) |
| 2026-02-07 11:24:42 +0100 | AlexNoo | (~AlexNoo@85.174.182.86) |
| 2026-02-07 11:24:19 +0100 | AlexNoo_ | (~AlexNoo@85.174.182.86) (Ping timeout: 260 seconds) |
| 2026-02-07 11:23:38 +0100 | Alex_delenda_est | (~al_test@85.174.181.199) (Ping timeout: 256 seconds) |
| 2026-02-07 11:23:28 +0100 | AlexNoo | (~AlexNoo@85.174.181.199) (Ping timeout: 246 seconds) |
| 2026-02-07 11:23:22 +0100 | <probie> | `Fresh` promises no name collisions, `Int` tells you the type, and `Var` tells you that it's a variable |
| 2026-02-07 11:22:50 +0100 | AlexZenon | (~alzenon@85.174.181.199) (Ping timeout: 245 seconds) |
| 2026-02-07 11:22:46 +0100 | <probie> | gentauro: What's wrong with it? |
| 2026-02-07 11:21:55 +0100 | peterbecich | (~Thunderbi@71.84.33.135) (Ping timeout: 264 seconds) |
| 2026-02-07 11:20:41 +0100 | AlexNoo__ | (~AlexNoo@85.174.182.86) |
| 2026-02-07 11:19:55 +0100 | AlexNoo_ | (~AlexNoo@85.174.182.86) |
| 2026-02-07 11:18:01 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-02-07 11:17:59 +0100 | gentauro | feels like: `AbstractAnimalThatLivesInWaterAndHasGillsAndFins.class` |
| 2026-02-07 11:16:42 +0100 | <gentauro> | `mkFreshIntVar` <- Hungarian notation for the win? Nah |
| 2026-02-07 11:12:58 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) (Ping timeout: 246 seconds) |
| 2026-02-07 11:12:47 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 11:09:04 +0100 | trickard_ | trickard |
| 2026-02-07 11:07:33 +0100 | <jreicher> | Codegen helps muddy the waters even further. |
| 2026-02-07 11:05:58 +0100 | <jreicher> | I think the defining characteristic of Lisp is "no code, everything is data" which is why it gets confused with the presentation of sexprs |
| 2026-02-07 11:04:53 +0100 | <jreicher> | Yes I think that's probably my point too. sexpr != lisp despite what everyone thinks |
| 2026-02-07 11:03:52 +0100 | <probie> | The Z3 monad is really just a codegen monad |
| 2026-02-07 11:03:12 +0100 | <probie> | They just chose S-expressions, because "everyone" in AI at the time was familiar with them |
| 2026-02-07 11:02:33 +0100 | <probie> | gentauro: There's very little lispy-ness in the SMTLIB2 format. It might as well be JSON, YAML or something entirely bespoke |
| 2026-02-07 11:01:57 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-02-07 10:57:40 +0100 | <jreicher> | What do you mean? Lisp is not great for stuff like this. |
| 2026-02-07 10:56:21 +0100 | trickard_ | (~trickard@cpe-61-98-47-163.wireline.com.au) |
| 2026-02-07 10:56:10 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 10:56:09 +0100 | trickard_ | (~trickard@cpe-61-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-02-07 10:56:00 +0100 | <gentauro> | I'm wondering how this (very Lisp'y) https://en.wikipedia.org/wiki/Z3_Theorem_Prover#Examples become like this https://github.com/IagoAbal/haskell-z3?tab=readme-ov-file#example |
| 2026-02-07 10:45:03 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 250 seconds) |
| 2026-02-07 10:43:19 +0100 | Enrico63 | (~Enrico63@host-79-27-153-69.retail.telecomitalia.it) Enrico63 |
| 2026-02-07 10:40:22 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 10:35:15 +0100 | trickard_ | (~trickard@cpe-61-98-47-163.wireline.com.au) |
| 2026-02-07 10:35:02 +0100 | trickard_ | (~trickard@cpe-61-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-02-07 10:34:49 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-02-07 10:34:44 +0100 | Inline | (~User@2a02:908:1246:26e0:ba5b:904f:46b4:eceb) Inline |
| 2026-02-07 10:33:15 +0100 | Inline | (~User@2a02:908:1246:26e0:807:305f:2053:3810) (Quit: KVIrc 5.0.0 Aria http://www.kvirc.net/) |
| 2026-02-07 10:29:30 +0100 | hsw | (~hsw@106.104.102.45) hsw |
| 2026-02-07 10:28:58 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-07 10:26:13 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2026-02-07 10:25:01 +0100 | hsw | (~hsw@106.104.102.45) (Quit: Leaving) |
| 2026-02-07 10:17:44 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |