Newest at the top
| 2025-01-16 13:50:32 +0100 | <kuribas> | tomsmeding: My goal is to have a verified implementation of https://www.cl.cam.ac.uk/~nk480/bidir.pdf, then add higher kinded types, type classes, data kinds and type families. |
| 2025-01-16 13:49:03 +0100 | <kuribas> | tomsmeding: a verified checker. |
| 2025-01-16 13:48:30 +0100 | <kuribas> | basically "forall (a:k) . t" |
| 2025-01-16 13:47:59 +0100 | <kuribas> | Forall : String -> (k:Kind) -> PolyType l -> PolyType l |
| 2025-01-16 13:47:35 +0100 | <kuribas> | tomsmeding: I've started a type checker in idris. I am using normal substitution for now. |
| 2025-01-16 13:46:31 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2025-01-16 13:46:11 +0100 | AlexNoo | (~AlexNoo@178.34.163.23) (Quit: Leaving) |
| 2025-01-16 13:44:50 +0100 | user363627 | (~user@user/user363627) (Remote host closed the connection) |
| 2025-01-16 13:42:56 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 2025-01-16 13:42:09 +0100 | AlexZenon | (~alzenon@178.34.163.23) (Quit: ;-) |
| 2025-01-16 13:40:21 +0100 | weary-traveler | (~user@user/user363627) (Ping timeout: 248 seconds) |
| 2025-01-16 13:36:20 +0100 | user363627 | (~user@user/user363627) user363627 |
| 2025-01-16 13:35:40 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-16 13:35:22 +0100 | euleritian | (~euleritia@dynamic-176-004-140-216.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-01-16 13:35:01 +0100 | euleritian | (~euleritia@dynamic-176-004-140-216.176.4.pool.telefonica.de) |
| 2025-01-16 13:34:52 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-01-16 13:32:56 +0100 | ColinRobinson | JuanDaugherty |
| 2025-01-16 13:30:37 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3505-d15c-e885-791c-fa20-9243.rev.sfr.net) alexherbo2 |
| 2025-01-16 13:28:43 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-01-16 13:26:51 +0100 | dnerdhm^ | (~dnerdhm@108.192.66.114) |
| 2025-01-16 13:25:12 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-01-16 13:21:53 +0100 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-01-16 13:12:11 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-16 13:11:31 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-01-16 13:10:52 +0100 | pointlessslippe1 | (~pointless@62.106.85.17) pointlessslippe1 |
| 2025-01-16 13:09:21 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-16 13:09:08 +0100 | Typedfern | (~Typedfern@248.red-83-37-32.dynamicip.rima-tde.net) typedfern |
| 2025-01-16 13:08:32 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-01-16 13:05:20 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-16 13:05:03 +0100 | euleritian | (~euleritia@dynamic-176-004-140-216.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-01-16 13:01:45 +0100 | caconym | (~caconym@user/caconym) caconym |
| 2025-01-16 13:01:25 +0100 | Digitteknohippie | Digit |
| 2025-01-16 13:01:21 +0100 | CiaoSen | (~Jura@2a05:5800:21a:4900:ca4b:d6ff:fec1:99da) (Ping timeout: 252 seconds) |
| 2025-01-16 13:00:46 +0100 | SlackCoder | (~SlackCode@64-94-63-8.ip.weststar.net.ky) SlackCoder |
| 2025-01-16 13:00:04 +0100 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2025-01-16 12:56:54 +0100 | tv | (~tv@user/tv) tv |
| 2025-01-16 12:55:53 +0100 | Typedfern | (~Typedfern@51.red-83-37-40.dynamicip.rima-tde.net) (Ping timeout: 244 seconds) |
| 2025-01-16 12:54:58 +0100 | euleritian | (~euleritia@dynamic-176-004-140-216.176.4.pool.telefonica.de) |
| 2025-01-16 12:54:28 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-01-16 12:52:19 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2025-01-16 12:51:23 +0100 | Typedfern | (~Typedfern@51.red-83-37-40.dynamicip.rima-tde.net) typedfern |
| 2025-01-16 12:48:36 +0100 | pointlessslippe1 | (~pointless@62.106.85.17) (Ping timeout: 252 seconds) |
| 2025-01-16 12:48:35 +0100 | notzmv | (~umar@user/notzmv) (Ping timeout: 252 seconds) |
| 2025-01-16 12:45:53 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-16 12:45:36 +0100 | euleritian | (~euleritia@dynamic-176-004-140-216.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-01-16 12:45:06 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Quit: ash3en) |
| 2025-01-16 12:44:17 +0100 | pointlessslippe1 | (~pointless@62.106.85.17) pointlessslippe1 |
| 2025-01-16 12:42:18 +0100 | dysthesis | (~dysthesis@user/dysthesis) (Remote host closed the connection) |
| 2025-01-16 12:40:55 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-01-16 12:38:31 +0100 | pointlessslippe- | (~pointless@62.106.85.17) (Quit: ZNC - http://znc.in) |