IRCBrowse

2026/03/12

Newest at the top

2026-03-12 20:07:24 +0100 <ski> it is the neutral element of the ambiguous operator `|'
2026-03-12 20:06:44 +0100 <ski> (in Haskell, you'd use `case ... of {}' for the absurd pattern case, e.g. with GADTs)
2026-03-12 20:06:09 +0100AlexNoo__(~AlexNoo@5.139.232.240)
2026-03-12 20:05:58 +0100Wygulmage(~Wygulmage@user/Wygulmage) (Ping timeout: 240 seconds)
2026-03-12 20:05:49 +0100 <ski> (but i allow using it in expressions, as well)
2026-03-12 20:05:25 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 20:05:22 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 20:05:20 +0100 <ski> `‾' means "undefined". in a pattern, in Agda, it's known as "absurd pattern", and spelled `()', used to indicate that we know no possible constructor could match
2026-03-12 20:05:00 +0100 <EvanR> what is ‾
2026-03-12 20:04:42 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 20:04:42 +0100 <EvanR> I was expecting to see - defined using ?< and ?< defined using - xD
2026-03-12 20:04:29 +0100 <Wygulmage88> Got to change locations. Gonna check the log.
2026-03-12 20:04:20 +0100 <EvanR> oh
2026-03-12 20:04:18 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 20:04:08 +0100 <ski> is the implementation
2026-03-12 20:04:00 +0100 <ski> Succ m - Succ n = m - n | Succ m ?< Succ n = m ?< n
2026-03-12 20:03:57 +0100 <ski> _ - Succ _ = ‾ | _ ?< Succ _ = ()
2026-03-12 20:03:51 +0100 <ski> m - Zero = m | _ ?< Zero = ‾
2026-03-12 20:03:50 +0100 <EvanR> oh
2026-03-12 20:03:46 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 20:03:29 +0100 <ski> yes
2026-03-12 20:02:58 +0100CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen
2026-03-12 20:02:46 +0100Wygulmage88(~Wygulmage@user/Wygulmage) Wygulmage
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)