Newest at the top
| 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 |
| 2025-01-14 13:35:19 +0100 | <ncf> | in Agda? you can if you replace Nat with Level |
| 2025-01-14 13:35:18 +0100 | <kuribas> | ncf: can I not write {n:Nat} -> {a:Type n} -> a -> a ? |
| 2025-01-14 13:34:06 +0100 | <ncf> | kuribas: implicits make no difference to universe levels |
| 2025-01-14 13:32:01 +0100 | <kuribas> | tomsmeding: a type is part of an AST, no? |
| 2025-01-14 13:30:22 +0100 | AlexNoo_ | AlexNoo |
| 2025-01-14 13:30:18 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 244 seconds) |
| 2025-01-14 13:28:41 +0100 | __monty__ | (~toonn@user/toonn) toonn |
| 2025-01-14 13:26:06 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2025-01-14 13:17:59 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-01-14 13:16:36 +0100 | akegalj_ | (~akegalj@89-172-71-66.adsl.net.t-com.hr) |
| 2025-01-14 13:11:16 +0100 | AlexZenon | (~alzenon@178.34.163.23) |
| 2025-01-14 13:05:59 +0100 | alecs | (~alecs@nat16.software.imdea.org) alecs |
| 2025-01-14 13:04:14 +0100 | AlexNoo | (~AlexNoo@178.34.160.135) (Ping timeout: 252 seconds) |
| 2025-01-14 13:04:14 +0100 | AlexZenon | (~alzenon@178.34.160.135) (Ping timeout: 244 seconds) |
| 2025-01-14 13:03:03 +0100 | caconym | (~caconym@user/caconym) caconym |
| 2025-01-14 13:00:59 +0100 | AlexNoo_ | (~AlexNoo@178.34.163.23) |
| 2025-01-14 13:00:04 +0100 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2025-01-14 12:59:59 +0100 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-01-14 12:58:09 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |