Newest at the top
| 2025-01-14 15:11:51 +0100 | <kuribas> | To make a work cloud? |
| 2025-01-14 15:11:44 +0100 | <kuribas> | hellwolf: did you finally find a way to use diagrams from a shell command? |
| 2025-01-14 15:11:16 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2025-01-14 15:08:46 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 244 seconds) |
| 2025-01-14 15:08:00 +0100 | ThePenguin | (~ThePengui@cust-95-80-24-166.csbnet.se) ThePenguin |
| 2025-01-14 15:05:47 +0100 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:28c7:5c1b:9c00:9e1b) ubert |
| 2025-01-14 15:03:06 +0100 | ThePenguin | (~ThePengui@cust-95-80-24-166.csbnet.se) (Remote host closed the connection) |
| 2025-01-14 14:59:55 +0100 | <hellwolf> | yea yea, next time sudo with password |
| 2025-01-14 14:59:38 +0100 | TheCoffeMaker | (~TheCoffeM@user/thecoffemaker) TheCoffeMaker |
| 2025-01-14 14:56:18 +0100 | michalz_ | (~michalz@185.246.207.203) |
| 2025-01-14 14:56:16 +0100 | michalz | (~michalz@185.246.207.197) (Read error: Connection reset by peer) |
| 2025-01-14 14:56:10 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-01-14 14:55:47 +0100 | alexherbo2 | (~alexherbo@2a02-8440-e501-2041-d1c5-ba5b-2b42-3c3f.rev.sfr.net) alexherbo2 |
| 2025-01-14 14:55:27 +0100 | alexherbo2 | (~alexherbo@2a02-8440-e501-2041-d1c5-ba5b-2b42-3c3f.rev.sfr.net) (Remote host closed the connection) |
| 2025-01-14 14:49:58 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2025-01-14 14:46:58 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-14 14:46:44 +0100 | akegalj_ | (~akegalj@89-172-71-66.adsl.net.t-com.hr) (Ping timeout: 248 seconds) |
| 2025-01-14 14:45:51 +0100 | <Hecate> | haha |
| 2025-01-14 14:44:23 +0100 | <kuribas> | hello_hellwolf.com helmsucks.yaml solves_halting_problem.hs get_rich_with_blockchain.rs |
| 2025-01-14 14:39:01 +0100 | tjbc | (~tjbc@user/fliife) fliife |
| 2025-01-14 14:37:53 +0100 | tjbc | (~tjbc@user/fliife) (Quit: ZNC - https://znc.in) |
| 2025-01-14 14:34:49 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 2025-01-14 14:33:23 +0100 | <hellwolf> | (sorry, wrong window) |
| 2025-01-14 14:33:23 +0100 | <hellwolf> | ls |
| 2025-01-14 14:29:26 +0100 | Fischmiep | (~Fischmiep@user/Fischmiep) Fischmiep |
| 2025-01-14 14:29:13 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-14 14:28:54 +0100 | Fischmiep | (~Fischmiep@user/Fischmiep) (Quit: ZNC - https://znc.in) |
| 2025-01-14 14:26:49 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2025-01-14 14:25:52 +0100 | Putonlalla | (~Putonlall@it-cyan.it.jyu.fi) Tuplanolla |
| 2025-01-14 14:23:15 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2025-01-14 14:21:02 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-14 14:19:43 +0100 | tv | (~tv@user/tv) tv |
| 2025-01-14 14:13:11 +0100 | <kuribas> | tomsmeding: My goal is to make a type checker in clojure, but I wanted to verify it in idris/agda first. |
| 2025-01-14 14:12:56 +0100 | <kuribas> | tomsmeding: yeah, maybe this doesn't make sense outside logic languages like twelf. |
| 2025-01-14 14:07:09 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
| 2025-01-14 14:05:06 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-14 14:03:43 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 2025-01-14 14:01:19 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-14 14:00:41 +0100 | <tomsmeding> | and then the question is, how strong is the type system of your embedded language |
| 2025-01-14 14:00:27 +0100 | <tomsmeding> | kuribas: a type is part of an AST, yes, but then you're talking about describing types in an embedded language, not in the host language. :p |
| 2025-01-14 13:59:36 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 2025-01-14 13:59:00 +0100 | tv | (~tv@user/tv) (Read error: Connection reset by peer) |
| 2025-01-14 13:50:30 +0100 | Putonlalla | (~Putonlall@it-cyan.it.jyu.fi) (Ping timeout: 252 seconds) |
| 2025-01-14 13:49:55 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 264 seconds) |
| 2025-01-14 13:41:46 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-14 13:41:46 +0100 | <kuribas> | ncf: not by design. I think universes are simply not yet implemented. |
| 2025-01-14 13:40:53 +0100 | <ncf> | idris 2 has Type : Type. you don't need universe polymorphism if there's only one universe! |
| 2025-01-14 13:38:37 +0100 | <kuribas> | https://docs.idris-lang.org/en/latest/faq/faq.html#does-idris-have-universe-polymorphism-what-is-tâĤ |
| 2025-01-14 13:38:35 +0100 | ephemient | (uid407513@user/ephemient) (Quit: Connection closed for inactivity) |
| 2025-01-14 13:36:03 +0100 | <ncf> | this means the exact same thing as (l : Level) â (a : Type l) â a â a except you don't have to write the arguments explicitly |