Newest at the top
| 2024-04-19 20:54:53 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-04-19 20:53:03 +0200 | xdminsy | (~xdminsy@117.147.70.233) (Remote host closed the connection) |
| 2024-04-19 20:50:16 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 256 seconds) |
| 2024-04-19 20:49:23 +0200 | Athas | (athas@sigkill.dk) |
| 2024-04-19 20:49:01 +0200 | Athas | (athas@sigkill.dk) (ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.3)) |
| 2024-04-19 20:48:41 +0200 | Square | (~Square@user/square) |
| 2024-04-19 20:46:35 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-04-19 20:45:50 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-04-19 20:45:50 +0200 | manifoldguy | (~dfs@72.183.132.110) (Quit: leaving) |
| 2024-04-19 20:44:59 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 264 seconds) |
| 2024-04-19 20:43:44 +0200 | <cheater> | what have i gotten myself into |
| 2024-04-19 20:43:41 +0200 | <cheater> | jesus |
| 2024-04-19 20:41:39 +0200 | <ncf> | (i guess it would be weird to emit a warning you can't do anything about?) |
| 2024-04-19 20:41:27 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) (Ping timeout: 272 seconds) |
| 2024-04-19 20:41:10 +0200 | tri_ | (~tri@2607:fb90:b1aa:d908:fc40:8b72:bf4a:f5c2) |
| 2024-04-19 20:40:49 +0200 | <ncf> | cheater: https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/overloaded_labels.html ? |
| 2024-04-19 20:39:31 +0200 | <ncf> | i don't know if that generates a warning though |
| 2024-04-19 20:39:08 +0200 | <ncf> | yin: let bindings use irrefutable patterns by default (so they are by definition exhaustive), but you can use ! to make them strict |
| 2024-04-19 20:38:29 +0200 | <cheater> | what is that stuff? |
| 2024-04-19 20:38:26 +0200 | <cheater> | i'm looking at this code base, and it has a lot of values the names of which start with # |
| 2024-04-19 20:38:23 +0200 | <lambdabot> | "*Exception: <interactive>:3:5-13: Non-exhaustive patterns in [] |
| 2024-04-19 20:38:21 +0200 | <ncf> | > let ![] = [0] in "a" |
| 2024-04-19 20:38:03 +0200 | <manifoldguy> | \who |
| 2024-04-19 20:37:33 +0200 | stef204 | (~stef204@user/stef204) (Quit: WeeChat 4.2.2) |
| 2024-04-19 20:37:12 +0200 | target_i | (~target_i@user/target-i/x-6023099) |
| 2024-04-19 20:36:10 +0200 | <yin> | is there a way to get warnings about non exaustive patterns in let bindings? |
| 2024-04-19 20:33:45 +0200 | demon-cat | (~demon-cat@vpn-fn-228.net.ed.ac.uk) (Ping timeout: 255 seconds) |
| 2024-04-19 20:32:48 +0200 | <monochrom> | Oh Andrej Bauer the what-is-algebraic-about-algebraic-effects guy! |
| 2024-04-19 20:30:48 +0200 | manifoldguy | (~dfs@72.183.132.110) |
| 2024-04-19 20:29:13 +0200 | <ncf> | (but maybe start with 01) |
| 2024-04-19 20:29:05 +0200 | demon-cat | (~demon-cat@vpn-fn-228.net.ed.ac.uk) |
| 2024-04-19 20:28:53 +0200 | <ncf> | that seems like a better starting point |
| 2024-04-19 20:28:44 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-04-19 20:27:47 +0200 | <monochrom> | But more seriously I think I will start from https://github.com/HoTT/EPIT-2020/tree/main/04-cubical-type-theory |
| 2024-04-19 20:27:13 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 2024-04-19 20:25:40 +0200 | <monochrom> | Haha "cubical type theory for dummies" https://gist.github.com/AndyShiue/cfc8c75f8b8655ca7ef2ffeb8cfb1faf/ (I haven't read it, I just find the title cute.) |
| 2024-04-19 20:24:20 +0200 | xdminsy | (~xdminsy@117.147.70.233) |
| 2024-04-19 20:10:33 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 256 seconds) |
| 2024-04-19 20:06:36 +0200 | xdminsy | (~xdminsy@117.147.70.233) (Remote host closed the connection) |
| 2024-04-19 20:00:06 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) (Ping timeout: 252 seconds) |
| 2024-04-19 19:51:19 +0200 | elbear | (~lucian@79.118.150.93) (Ping timeout: 268 seconds) |
| 2024-04-19 19:50:21 +0200 | <tomsmeding> | dolio: I see :) |
| 2024-04-19 19:48:47 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-04-19 19:47:23 +0200 | <dolio> | The more rigorous Martin-löf type theory is similarly inadequate. It basically only works for inductive definitions (in its sense, which does not match Haskell's). |
| 2024-04-19 19:45:08 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-04-19 19:45:07 +0200 | Etabeta1 | (~Etabeta1@151.30.10.212) |
| 2024-04-19 19:42:30 +0200 | philopsos | (~caecilius@user/philopsos) (Ping timeout: 252 seconds) |
| 2024-04-19 19:41:39 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 2024-04-19 19:40:21 +0200 | <monochrom> | :) |
| 2024-04-19 19:40:13 +0200 | <ncf> | it's a HoTT take &c |