Newest at the top
| 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) |
| 2025-01-14 12:57:51 +0100 | euleritian | (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-01-14 12:57:12 +0100 | dysthesis | (~dysthesis@user/dysthesis) (Remote host closed the connection) |
| 2025-01-14 12:55:07 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2025-01-14 12:53:32 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-01-14 12:52:48 +0100 | euphores | (~SASL_euph@user/euphores) (Ping timeout: 246 seconds) |
| 2025-01-14 12:50:21 +0100 | euleritian | (~euleritia@dynamic-176-006-133-187.176.6.pool.telefonica.de) |
| 2025-01-14 12:50:13 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 248 seconds) |
| 2025-01-14 12:49:53 +0100 | alecs | (~alecs@nat16.software.imdea.org) (Ping timeout: 252 seconds) |
| 2025-01-14 12:48:33 +0100 | ChanServ | +v haskellbridge |
| 2025-01-14 12:48:33 +0100 | haskellbridge | (~hackager@syn-024-093-192-219.res.spectrum.com) hackager |
| 2025-01-14 12:47:31 +0100 | haskellbridge | (~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection) |
| 2025-01-14 12:43:05 +0100 | alexherbo2 | (~alexherbo@2a02-8440-e501-2041-d1c5-ba5b-2b42-3c3f.rev.sfr.net) alexherbo2 |
| 2025-01-14 12:42:32 +0100 | alexherbo2 | (~alexherbo@2a02-8440-e501-2041-d1c5-ba5b-2b42-3c3f.rev.sfr.net) (Remote host closed the connection) |
| 2025-01-14 12:37:43 +0100 | dmwit | (~dmwit@pool-173-66-76-243.washdc.fios.verizon.net) (Quit: Client closed) |
| 2025-01-14 12:36:51 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2025-01-14 12:36:06 +0100 | alexherbo2 | (~alexherbo@2a02-8440-e501-2041-d1c5-ba5b-2b42-3c3f.rev.sfr.net) alexherbo2 |
| 2025-01-14 12:33:38 +0100 | jespada | (~jespada@2800:a4:31:b00:a974:16da:8c45:e3b4) jespada |
| 2025-01-14 12:26:22 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-14 12:24:13 +0100 | dysthesis | (~dysthesis@user/dysthesis) dysthesis |
| 2025-01-14 12:16:23 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2025-01-14 12:13:59 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
| 2025-01-14 12:13:29 +0100 | xff0x | (~xff0x@2405:6580:b080:900:5599:62cc:9825:4e0a) |
| 2025-01-14 12:10:06 +0100 | <tomsmeding> | is HOAS not more about representing an AST? |
| 2025-01-14 12:10:04 +0100 | <kuribas> | tomsmeding: I was just considering this: https://en.wikipedia.org/wiki/Higher-order_abstract_syntax |
| 2025-01-14 12:10:04 +0100 | akegalj | (~akegalj@89-172-71-66.adsl.net.t-com.hr) (Ping timeout: 244 seconds) |
| 2025-01-14 12:09:25 +0100 | Miroboru | (~myrvoll@178-164-114.82.3p.ntebredband.no) Miroboru |
| 2025-01-14 12:08:55 +0100 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) kuribas |