| 2025-05-04 00:00:15 +0200 | tromp | (~textual@2001:1c00:3487:1b00:31c9:5f27:18bf:4d4e) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-04 00:04:06 +0200 | P1RATEZ | (piratez@user/p1ratez) (Quit: Going offline, see ya! (www.adiirc.com)) |
| 2025-05-04 00:09:27 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) |
| 2025-05-04 00:15:09 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) (Ping timeout: 252 seconds) |
| 2025-05-04 00:16:12 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 2025-05-04 00:22:19 +0200 | Buliarous | (~gypsydang@46.232.210.139) (Remote host closed the connection) |
| 2025-05-04 00:22:48 +0200 | Buliarous | (~gypsydang@46.232.210.139) Buliarous |
| 2025-05-04 00:23:52 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-04 00:32:36 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2025-05-04 00:56:36 +0200 | nacation | (~m-3l4s76@user/nacation) (Ping timeout: 252 seconds) |
| 2025-05-04 00:57:45 +0200 | j1n37- | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-05-04 01:00:43 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 01:00:51 +0200 | nacation | (~m-3l4s76@user/nacation) nacation |
| 2025-05-04 01:08:53 +0200 | preflex_ | (~preflex@user/mauke/bot/preflex) preflex |
| 2025-05-04 01:10:37 +0200 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-05-04 01:12:29 +0200 | preflex | (~preflex@user/mauke/bot/preflex) (Ping timeout: 245 seconds) |
| 2025-05-04 01:12:47 +0200 | preflex_ | preflex |
| 2025-05-04 01:14:40 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 272 seconds) |
| 2025-05-04 01:14:41 +0200 | ljdarj1 | ljdarj |
| 2025-05-04 01:15:34 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) chiselfuse |
| 2025-05-04 01:15:43 +0200 | tremon | (~tremon@83.80.159.219) (Quit: getting boxed in) |
| 2025-05-04 01:33:43 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f7604057216e123cf7a.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2025-05-04 01:40:00 +0200 | joeyadams | (~textual@syn-162-154-010-038.res.spectrum.com) |
| 2025-05-04 01:42:22 +0200 | hiredman | (~hiredman@frontier1.downey.family) (Quit: Lost terminal) |
| 2025-05-04 01:46:12 +0200 | la1n2 | (~la1n@176.59.166.253) (Read error: Connection reset by peer) |
| 2025-05-04 01:47:58 +0200 | la1n2 | (~la1n@176.59.56.11) |
| 2025-05-04 01:53:42 +0200 | AlexZenon_2 | (~alzenon@5.139.233.9) |
| 2025-05-04 01:55:15 +0200 | la1n23 | (~la1n@109.197.206.191) |
| 2025-05-04 01:55:16 +0200 | AlexZenon | (~alzenon@5.139.233.9) (Ping timeout: 252 seconds) |
| 2025-05-04 01:55:22 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess |
| 2025-05-04 01:57:50 +0200 | la1n2 | (~la1n@176.59.56.11) (Ping timeout: 252 seconds) |
| 2025-05-04 01:58:55 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-05-04 01:59:29 +0200 | euleritian | (~euleritia@dynamic-176-006-135-247.176.6.pool.telefonica.de) |
| 2025-05-04 02:07:14 +0200 | hiecaq | (~hiecaq@user/hiecaq) hiecaq |
| 2025-05-04 02:09:49 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2025-05-04 02:12:33 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 248 seconds) |
| 2025-05-04 02:14:51 +0200 | sprotte24 | (~sprotte24@p200300d16f17ff001d650b9c3df58534.dip0.t-ipconnect.de) (Quit: Leaving) |
| 2025-05-04 02:17:21 +0200 | Pozyomka | (~pyon@user/pyon) pyon |
| 2025-05-04 02:20:31 +0200 | sajenim | (~sajenim@user/sajenim) sajenim |
| 2025-05-04 02:51:04 +0200 | gabriel_sevecek | (~gabriel@188-167-229-200.dynamic.chello.sk) (Ping timeout: 276 seconds) |
| 2025-05-04 02:51:33 +0200 | gabriel_sevecek | (~gabriel@188-167-229-200.dynamic.chello.sk) gabriel_sevecek |
| 2025-05-04 03:05:46 +0200 | bilegeek | (~bilegeek@2600:1008:b01a:5c24:8c91:aa31:8c9:aaf) (Quit: Leaving) |
| 2025-05-04 03:07:45 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2025-05-04 03:20:58 +0200 | hiecaq | (~hiecaq@user/hiecaq) (Quit: ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.0.92)) |
| 2025-05-04 03:21:26 +0200 | __jmcantrell__ | (~weechat@user/jmcantrell) (Quit: WeeChat 4.6.2) |
| 2025-05-04 03:28:19 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 245 seconds) |
| 2025-05-04 03:28:26 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 03:39:09 +0200 | jackdk | (sid373013@cssa/jackdk) (Changing host) |
| 2025-05-04 03:39:09 +0200 | jackdk | (sid373013@cssa/life/jackdk) jackdk |
| 2025-05-04 03:40:49 +0200 | __jmcantrell__ | (~weechat@user/jmcantrell) jmcantrell |
| 2025-05-04 03:42:02 +0200 | j1n37- | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-05-04 03:45:53 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 03:46:10 +0200 | ttybitnik | (~ttybitnik@user/wolper) (Quit: Fading out...) |
| 2025-05-04 04:05:01 +0200 | op_4 | (~tslil@user/op-4/x-9116473) (Remote host closed the connection) |
| 2025-05-04 04:05:36 +0200 | op_4 | (~tslil@user/op-4/x-9116473) op_4 |
| 2025-05-04 04:08:49 +0200 | xff0x | (~xff0x@2405:6580:b080:900:7099:7f52:1441:1e43) (Ping timeout: 248 seconds) |
| 2025-05-04 04:12:52 +0200 | typedfern_ | (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) |
| 2025-05-04 04:13:42 +0200 | Typedfern | (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) (Ping timeout: 276 seconds) |
| 2025-05-04 04:15:49 +0200 | td_ | (~td@i53870919.versanet.de) (Ping timeout: 248 seconds) |
| 2025-05-04 04:17:38 +0200 | td_ | (~td@i53870915.versanet.de) |
| 2025-05-04 04:21:12 +0200 | ystael | (~ystael@user/ystael) (Ping timeout: 252 seconds) |
| 2025-05-04 04:23:24 +0200 | tolgo | (~Thunderbi@199.115.144.130) |
| 2025-05-04 04:44:00 +0200 | euleritian | (~euleritia@dynamic-176-006-135-247.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-05-04 04:48:43 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-05-04 05:00:31 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2025-05-04 05:00:31 +0200 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2025-05-04 05:00:50 +0200 | califax | (~califax@user/califx) califx |
| 2025-05-04 05:01:14 +0200 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2025-05-04 05:21:56 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2025-05-04 05:22:31 +0200 | xff0x | (~xff0x@2405:6580:b080:900:e1a9:cd8e:4cbb:591b) |
| 2025-05-04 05:36:10 +0200 | infinity0 | (~infinity0@pwned.gg) (Ping timeout: 276 seconds) |
| 2025-05-04 05:36:52 +0200 | infinity0 | (~infinity0@pwned.gg) infinity0 |
| 2025-05-04 05:38:12 +0200 | tomku | (~tomku@user/tomku) (Ping timeout: 276 seconds) |
| 2025-05-04 05:42:36 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 05:43:34 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 260 seconds) |
| 2025-05-04 05:44:33 +0200 | tomku | (~tomku@user/tomku) tomku |
| 2025-05-04 05:47:49 +0200 | aforemny_ | (~aforemny@i59F4C6FD.versanet.de) aforemny |
| 2025-05-04 05:48:06 +0200 | aforemny | (~aforemny@i59F4C605.versanet.de) (Ping timeout: 252 seconds) |
| 2025-05-04 06:08:54 +0200 | <haskellbridge> | <hellwolf> Huh? |
| 2025-05-04 06:09:05 +0200 | <haskellbridge> | <hellwolf> sonic boom? |
| 2025-05-04 06:15:26 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 06:15:58 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-05-04 06:16:19 +0200 | <haskellbridge> | <hellwolf> anyways, today is the day to confront the demon... |
| 2025-05-04 06:16:19 +0200 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/xIZbjVwEiWebhDhhUHdAQgaI/rbHeUYfmCGw (4 lines) |
| 2025-05-04 06:18:03 +0200 | <monochrom> | I think for sum types you go for prisms rather than lenses. |
| 2025-05-04 06:23:10 +0200 | <haskellbridge> | <hellwolf> makePrisms |
| 2025-05-04 06:23:54 +0200 | <haskellbridge> | <hellwolf> let me see that i can learn there. |
| 2025-05-04 06:23:54 +0200 | <haskellbridge> | also, should i use generics-sop, though i would need code examples... |
| 2025-05-04 06:27:05 +0200 | <haskellbridge> | <hellwolf> https://hackage-content.haskell.org/package/lens-5.3.4/docs/src/Control.Lens.Internal.PrismTH.html… |
| 2025-05-04 06:27:07 +0200 | <haskellbridge> | not too many lines to learn. it seems. i am relieved |
| 2025-05-04 06:29:37 +0200 | sim590 | (~simon@209-15-185-101.resi.cgocable.ca) (Ping timeout: 248 seconds) |
| 2025-05-04 06:52:13 +0200 | tolgo | (~Thunderbi@199.115.144.130) (Ping timeout: 276 seconds) |
| 2025-05-04 06:56:21 +0200 | <haskellbridge> | <hellwolf> "isn't :: Prism s t a b -> s -> Bool" |
| 2025-05-04 06:56:21 +0200 | <haskellbridge> | finally i see others using the single quote in names... |
| 2025-05-04 06:56:45 +0200 | <monochrom> | :) |
| 2025-05-04 06:59:21 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-05-04 07:16:05 +0200 | <EvanR> | ahem |
| 2025-05-04 07:16:18 +0200 | <EvanR> | please. apostrophe |
| 2025-05-04 07:35:04 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 07:35:10 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-05-04 07:44:10 +0200 | bitmapper | (uid464869@id-464869.lymington.irccloud.com) bitmapper |
| 2025-05-04 07:59:18 +0200 | joeyadams | (~textual@syn-162-154-010-038.res.spectrum.com) (Quit: Textual IRC Client: www.textualapp.com) |
| 2025-05-04 08:05:52 +0200 | __jmcantrell__ | (~weechat@user/jmcantrell) (Ping timeout: 244 seconds) |
| 2025-05-04 08:13:07 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-05-04 08:23:21 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 2025-05-04 08:24:13 +0200 | haritz | (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 2025-05-04 08:25:57 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f7604057216e123cf7a.dip0.t-ipconnect.de) acidjnk |
| 2025-05-04 08:26:36 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) |
| 2025-05-04 08:32:17 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 08:32:44 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 260 seconds) |
| 2025-05-04 08:37:54 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2025-05-04 08:46:57 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-05-04 08:53:50 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-04 09:00:00 +0200 | caconym7 | (~caconym@user/caconym) (Quit: bye) |
| 2025-05-04 09:00:38 +0200 | caconym7 | (~caconym@user/caconym) caconym |
| 2025-05-04 09:01:32 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) |
| 2025-05-04 09:04:44 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-05-04 09:07:14 +0200 | la1n2 | (~la1n@81.222.176.125) |
| 2025-05-04 09:09:53 +0200 | la1n23 | (~la1n@109.197.206.191) (Ping timeout: 265 seconds) |
| 2025-05-04 09:22:39 +0200 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-05-04 09:23:45 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 276 seconds) |
| 2025-05-04 09:24:02 +0200 | Lord_of_Life_ | Lord_of_Life |
| 2025-05-04 09:25:41 +0200 | <haskellbridge> | <hellwolf> what's the reason for classy lenses or prisma? It's non obvious to me, and the docs doesn't explain the "why" |
| 2025-05-04 09:40:04 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 272 seconds) |
| 2025-05-04 09:52:20 +0200 | __monty__ | (~toonn@user/toonn) toonn |
| 2025-05-04 10:32:55 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2025-05-04 10:35:02 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2025-05-04 10:35:04 +0200 | <jackdk> | hellwolf: https://youtu.be/GZPup5Iuaqw?t=1499 (note the timecode, though the whole talk is good) |
| 2025-05-04 10:50:59 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 2025-05-04 10:57:16 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 2025-05-04 10:57:39 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) |
| 2025-05-04 11:08:06 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f7604057216e123cf7a.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 2025-05-04 11:10:29 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |
| 2025-05-04 11:13:08 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f525d73c8bc79cfad4f.dip0.t-ipconnect.de) |
| 2025-05-04 11:16:27 +0200 | <haskellbridge> | <hellwolf> thank you! checking now |
| 2025-05-04 11:21:57 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2025-05-04 11:22:22 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2025-05-04 11:37:12 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-05-04 11:47:19 +0200 | Square | (~Square@user/square) (Ping timeout: 276 seconds) |
| 2025-05-04 11:51:05 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-04 12:00:10 +0200 | poscat | (~poscat@user/poscat) poscat |
| 2025-05-04 12:04:37 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) |
| 2025-05-04 12:05:04 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) (Ping timeout: 260 seconds) |
| 2025-05-04 12:14:42 +0200 | poscat | (~poscat@user/poscat) (Remote host closed the connection) |
| 2025-05-04 12:15:17 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 248 seconds) |
| 2025-05-04 12:16:50 +0200 | poscat | (~poscat@user/poscat) poscat |
| 2025-05-04 12:27:57 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2025-05-04 12:31:27 +0200 | <hellwolf> | I watched it. TL;DV: to index optical operations into one type class, so that you can stack them up in your application monad. It's probably obvious if you actually build such a application that deal with real world :) |
| 2025-05-04 12:33:27 +0200 | <Rembane> | That sounds neat |
| 2025-05-04 12:36:50 +0200 | <hellwolf> | I wish the docs actually care to give just a few lines of "why". But I guess it risks of being too brief and confuses some people. Not sure what's the good middle ground of these sort of things is. |
| 2025-05-04 12:38:34 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) wootehfoot |
| 2025-05-04 12:45:48 +0200 | aljazmc | (~aljazmc@user/aljazmc) aljazmc |
| 2025-05-04 12:52:13 +0200 | gabiruh | (~gabiruh@vps19177.publiccloud.com.br) (Ping timeout: 265 seconds) |
| 2025-05-04 12:53:03 +0200 | hiecaq | (~hiecaq@user/hiecaq) hiecaq |
| 2025-05-04 13:00:43 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) |
| 2025-05-04 13:07:29 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2025-05-04 13:07:59 +0200 | aljazmc | (~aljazmc@user/aljazmc) (Quit: Leaving) |
| 2025-05-04 13:08:16 +0200 | aljazmc | (~aljazmc@user/aljazmc) aljazmc |
| 2025-05-04 13:13:44 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f525d73c8bc79cfad4f.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2025-05-04 13:16:15 +0200 | gabiruh | (~gabiruh@vps19177.publiccloud.com.br) gabiruh |
| 2025-05-04 13:25:08 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f524d98fe298d45bbdf.dip0.t-ipconnect.de) |
| 2025-05-04 13:38:10 +0200 | euphores | (~SASL_euph@user/euphores) (Ping timeout: 252 seconds) |
| 2025-05-04 13:45:09 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-05-04 13:51:28 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2025-05-04 13:51:45 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-05-04 13:52:15 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-05-04 13:58:36 +0200 | <[exa]> | are there some good "small" libraries theorem proving? E.g. I've got an algebra, a few axioms on it, and I want to see how the axioms can be combined to derive some expression in the algebra. Ideally if axiom schemes are supported. |
| 2025-05-04 13:58:47 +0200 | <[exa]> | s/if // |
| 2025-05-04 14:01:26 +0200 | <[exa]> | the issue with the theorem provers I see is that they kinda assume some particular fixed algebra (some kind of logic), I need some freedom in there without having to encode stuff too much. |
| 2025-05-04 14:04:14 +0200 | <tomsmeding> | prolog? |
| 2025-05-04 14:05:46 +0200 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2025-05-04 14:11:57 +0200 | tolgo | (~Thunderbi@199.115.144.130) |
| 2025-05-04 14:14:12 +0200 | tolgo | (~Thunderbi@199.115.144.130) (Client Quit) |
| 2025-05-04 14:15:19 +0200 | <[exa]> | tomsmeding: yeah like I could go full ListT but I guess it will need heuristics |
| 2025-05-04 14:16:02 +0200 | <[exa]> | s/List/Logic/ |
| 2025-05-04 14:21:16 +0200 | <tomsmeding> | I mean you can actually model a proof checker, but at that point you're writing what you're asking already exists, I guess :p |
| 2025-05-04 14:21:47 +0200 | <tomsmeding> | what kind of things do you want to prove? |
| 2025-05-04 14:22:24 +0200 | <tomsmeding> | and do you want there to be proof search or just checking of manual proofs |