IRCBrowse

2026/03/12

Newest at the top

2026-03-12 20:00:48 +0100AlexNoo__(~AlexNoo@5.139.232.240)
2026-03-12 20:00:30 +0100 <EvanR> the implementation of what exactly, both these operators?
2026-03-12 20:00:04 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 20:00:02 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:59:54 +0100 <ski> it wasn't shown. i just showed the type signature, not the implementation
2026-03-12 19:59:38 +0100 <EvanR> where is the { ... } in the original notation
2026-03-12 19:59:21 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 19:59:11 +0100arandombit(~arandombi@user/arandombit) arandombit
2026-03-12 19:59:11 +0100arandombit(~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host)
2026-03-12 19:59:11 +0100arandombit(~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c)
2026-03-12 19:59:02 +0100 <ski> { ... }
2026-03-12 19:58:58 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:58:58 +0100 <ski> nat m,n;
2026-03-12 19:58:57 +0100Googulator38(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
2026-03-12 19:58:51 +0100 <ski> nat minus(m,n) | void under(m,n)
2026-03-12 19:58:47 +0100 <ski> if you prefer a more C-like syntax :
2026-03-12 19:58:41 +0100Googulator38(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed)
2026-03-12 19:58:28 +0100 <EvanR> oof ok
2026-03-12 19:58:26 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:56:28 +0100 <ski> ("-" | "?<") , ":" , ("|" , ",") , "-|"
2026-03-12 19:56:19 +0100 <ski> er, forgot to insert the `:' ..
2026-03-12 19:55:54 +0100 <ski> (((k / n) : Fin m) , ((k % n) : Fin n)) -| ((m : Nat) , (n : Nat) , (k : Fin (m * n)))
2026-03-12 19:55:28 +0100AlexNoo__(~AlexNoo@5.139.232.240)
2026-03-12 19:55:22 +0100 <ski> (((k - m) : Fin n) | ((k ?< m) : Fin m)) -| ((m : Nat) , (n : Nat) , (k : Fin (m + n)))
2026-03-12 19:54:50 +0100 <Wygulmage> Thanks, I was not parsing it like that.
2026-03-12 19:54:44 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 19:54:42 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:54:12 +0100 <ski> ((m - n) : Nat) | ((m ?< n) : ()) -| ((m : Nat) , (n : Nat))
2026-03-12 19:54:01 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 19:53:39 +0100 <ski> ("-" | "?<") , ("|" , ",") , "-|"
2026-03-12 19:53:38 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:53:06 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:52:15 +0100 <EvanR> there's so much punctuation in m - n : Nat | m ?< n : () -| m : Nat , n : Nat let me try to guess the precedence from highest to lowest: : - ?< , | -|
2026-03-12 19:51:05 +0100 <ski> Wygulmage : if you want to, you could say `Right (k - m) | Left (k ?< m)' produces a sum type (`Fin m + Fin n')
2026-03-12 19:50:08 +0100AlexNoo__(~AlexNoo@5.139.232.240)
2026-03-12 19:50:07 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
2026-03-12 19:49:32 +0100 <ski> (there's a reason why i'm making some of the arguments `Nat's and others `Fin o's for various `o's, here, but it's a bit incidental to the general idea of "simultaneous alternative definitions"")
2026-03-12 19:49:25 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 19:49:22 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:48:42 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 19:48:18 +0100peterbecich(~Thunderbi@71.84.33.135) (Ping timeout: 248 seconds)
2026-03-12 19:48:18 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:48:05 +0100Googulator38(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
2026-03-12 19:47:52 +0100 <ski> in the dependently typed version, `k ?< m : Fin m', but you could, if you wanted, make that `k ?< m : k < m' (modulo an inclusion from `Fin (m + n)' to `Nat' for the `k'), instead
2026-03-12 19:47:50 +0100Googulator38(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed)
2026-03-12 19:47:46 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:46:56 +0100 <ski> `?<' (if it terminates, is not partial) provides evidence of the `<' relation between the inputs
2026-03-12 19:45:59 +0100 <ski> Wygulmage : neither
2026-03-12 19:45:38 +0100 <ski> (quick, what's the result of `k / 0' and `k % 0' ?)
2026-03-12 19:45:27 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn