Newest at the top
| 2025-01-16 14:13:53 +0100 | xff0x | (~xff0x@2405:6580:b080:900:cb37:dc44:25ad:be87) (Ping timeout: 248 seconds) |
| 2025-01-16 14:13:30 +0100 | Digitteknohippie | (~user@user/digit) Digit |
| 2025-01-16 14:12:28 +0100 | <lambdabot> | * |
| 2025-01-16 14:12:27 +0100 | <kuribas> | :k * -> * |
| 2025-01-16 14:12:11 +0100 | <kuribas> | Is '* -> *' considered a type? |
| 2025-01-16 14:06:43 +0100 | xff0x | (~xff0x@2405:6580:b080:900:cb37:dc44:25ad:be87) |
| 2025-01-16 14:05:54 +0100 | rvalue- | rvalue |
| 2025-01-16 14:04:27 +0100 | PHO` | (~pho@akari.cielonegro.org) PHO` |
| 2025-01-16 14:03:46 +0100 | xff0x | (~xff0x@2405:6580:b080:900:d12f:67f5:c2b0:5368) (Ping timeout: 248 seconds) |
| 2025-01-16 14:00:21 +0100 | PHO` | (~pho@akari.cielonegro.org) (Quit: SIGTERM received; exit) |
| 2025-01-16 14:00:12 +0100 | ec | (~ec@gateway/tor-sasl/ec) (Ping timeout: 264 seconds) |
| 2025-01-16 13:59:58 +0100 | housemate | (~housemate@146.70.66.228) housemate |
| 2025-01-16 13:59:44 +0100 | Guest38 | (~Guest38@2a02:a03f:c0fd:e500:6c68:1cd6:8c4:155f) (Client Quit) |
| 2025-01-16 13:58:43 +0100 | Guest38 | (~Guest38@2a02:a03f:c0fd:e500:6c68:1cd6:8c4:155f) |
| 2025-01-16 13:58:04 +0100 | rvalue- | (~rvalue@user/rvalue) rvalue |
| 2025-01-16 13:57:53 +0100 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 252 seconds) |
| 2025-01-16 13:57:47 +0100 | notzmv | (~umar@user/notzmv) notzmv |
| 2025-01-16 13:57:13 +0100 | Square2 | (~Square4@user/square) Square |
| 2025-01-16 13:57:12 +0100 | xff0x | (~xff0x@2405:6580:b080:900:d12f:67f5:c2b0:5368) |
| 2025-01-16 13:55:06 +0100 | xff0x | (~xff0x@2405:6580:b080:900:7761:255c:77e5:46e1) (Quit: xff0x) |
| 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) |