Newest at the top
| 2025-02-25 00:21:58 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-25 00:20:23 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 245 seconds) |
| 2025-02-25 00:20:17 +0100 | malte | (~malte@mal.tc) malte |
| 2025-02-25 00:18:12 +0100 | zungi | (~tory@user/andrewchawk) (Ping timeout: 264 seconds) |
| 2025-02-25 00:17:49 +0100 | malte | (~malte@mal.tc) (Remote host closed the connection) |
| 2025-02-25 00:14:01 +0100 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2025-02-25 00:12:14 +0100 | AlexNoo | (~AlexNoo@178.34.162.44) |
| 2025-02-25 00:11:25 +0100 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2025-02-25 00:11:12 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2025-02-25 00:09:59 +0100 | AlexNoo | (~AlexNoo@178.34.162.44) (Read error: Connection reset by peer) |
| 2025-02-25 00:09:12 +0100 | malte | (~malte@mal.tc) malte |
| 2025-02-25 00:07:12 +0100 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2025-02-25 00:06:10 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-25 00:00:34 +0100 | olivial | (~benjaminl@user/benjaminl) (Ping timeout: 260 seconds) |
| 2025-02-24 23:58:05 +0100 | olivial_ | (~benjaminl@c-76-144-12-233.hsd1.or.comcast.net) |
| 2025-02-24 23:57:22 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2025-02-24 23:57:09 +0100 | stm32nucleo | (~stm32nucl@2a02:1210:545d:200:a978:119d:8aba:7f6e) (Quit: Client closed) |
| 2025-02-24 23:56:13 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 245 seconds) |
| 2025-02-24 23:55:21 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 2025-02-24 23:52:00 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 23:50:32 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 23:49:10 +0100 | ColinRobinson | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 2025-02-24 23:49:07 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-02-24 23:40:01 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-02-24 23:37:46 +0100 | stm32nucleo | (~stm32nucl@2a02:1210:545d:200:a978:119d:8aba:7f6e) |
| 2025-02-24 23:35:09 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 23:25:51 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-02-24 23:23:58 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-02-24 23:23:20 +0100 | <EvanR> | parenthesized by braces, braced by brackets, and bracketed by parentheses |
| 2025-02-24 23:22:54 +0100 | <monochrom> | I guess Coq's is like "Type @{...}" so it is parenthesized, by curry braces. |
| 2025-02-24 23:19:47 +0100 | <monochrom> | But you would need the parens in Lean. :) |
| 2025-02-24 23:19:43 +0100 | <ncf> | average coq documentation experience |
| 2025-02-24 23:19:38 +0100 | <ncf> | there seems to be syntax for specifying levels explicitly but i can't tell how it works https://coq.inria.fr/doc/V8.18.0/refman/language/core/sorts.html#sorts |
| 2025-02-24 23:19:26 +0100 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-02-24 23:19:19 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 23:18:01 +0100 | <monochrom> | Coq does not allow you to write "Type n" or "Type (n+1)". It only lets you write "Type" and it infers the level. |
| 2025-02-24 23:17:28 +0100 | <EvanR> | do you need the parens in Coq |
| 2025-02-24 23:16:59 +0100 | <EvanR> | lol |
| 2025-02-24 23:16:56 +0100 | <EvanR> | now I won't know |
| 2025-02-24 23:16:41 +0100 | <monochrom> | "Type n : Type (n+1)" |
| 2025-02-24 23:16:34 +0100 | <monochrom> | :( |
| 2025-02-24 23:15:58 +0100 | <EvanR> | is the precedence of Type _ really less than addition there |
| 2025-02-24 23:14:52 +0100 | <monochrom> | Bad habit from Coq I guess. You just write "Type" and it means "Type n" where n is inferred from context. So you write "Type : Type" and it is nothing paradoxical, it is inferred to be "Type n : Type n+1" |
| 2025-02-24 23:14:24 +0100 | <tomsmeding> | but if the answer to that question is "it's in U", then you might as well just destroy all Un with n >= 1, because you'll never need them, and then U = U0 because there's only one universe |
| 2025-02-24 23:14:07 +0100 | Ekho | (~Ekho@user/ekho) Ekho |
| 2025-02-24 23:13:39 +0100 | tromp | (~textual@2a02:a210:cba:8500:6ddc:c1a9:bc13:1391) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-02-24 23:13:36 +0100 | <tomsmeding> | for example U0 |
| 2025-02-24 23:13:31 +0100 | <EvanR> | shoot |
| 2025-02-24 23:13:25 +0100 | <tomsmeding> | I meant U for any Un |
| 2025-02-24 23:13:20 +0100 | <tomsmeding> | sorry |