Newest at the top
| 2026-03-12 20:24:25 +0100 | <ski> | types have to match |
| 2026-03-12 20:23:02 +0100 | <EvanR> | and the types don't have to match immediately |
| 2026-03-12 20:22:25 +0100 | <EvanR> | so the Succ ((m - n) / n) will be "tried" first and if it's undefined go to the thing right of | |
| 2026-03-12 20:22:09 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:21:25 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:21:22 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:20:51 +0100 | <ski> | (that does not terminate for `n = 0'. dependently typed version i hinted at above is total, though) |
| 2026-03-12 20:20:51 +0100 | Ranhir | (~Ranhir@157.97.53.139) (Ping timeout: 246 seconds) |
| 2026-03-12 20:20:42 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:20:20 +0100 | <ski> | m / n = Succ ((m - n) / n) | let () = m ?< n in Zero ; m % n = (m - n) % n | let () = m ?< n in m |
| 2026-03-12 20:20:18 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:19:46 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:17:19 +0100 | <EvanR> | what does applying both operators look like |
| 2026-03-12 20:17:02 +0100 | <ski> | (if you're just using one of them, it would be partial, yes) |
| 2026-03-12 20:16:49 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:16:49 +0100 | <ski> | nope, because you're supposed to pair up an application of `-', with an application of `?<' so that one of them will be defined, succeed |
| 2026-03-12 20:16:05 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:16:02 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:15:38 +0100 | <EvanR> | so the program will crash or |
| 2026-03-12 20:15:24 +0100 | <EvanR> | Zero - Succ _ = undefined |
| 2026-03-12 20:15:22 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:14:58 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:14:26 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:14:25 +0100 | <ski> | (btw, for the dependently typed version, you'd replace the latter two right side definitions by `Zero ?< Succ _ = Zero' and `Succ m ?< Succ n = Succ (m ?< n)', so `k ?< m' here is equal to `k', but restricted to be an element of `Fin m', rather than an element of `Fin (m + n)') |
| 2026-03-12 20:13:24 +0100 | <ski> | oh .. sorry, i just realized the left argument of the middle equations should be `Zero', not `_' (was taking this from memory). hopefully that makes more sense (removing the inadvertent overlap between the equations) |
| 2026-03-12 20:11:29 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:10:45 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:10:42 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:10:28 +0100 | Wygulmage88 | (~Wygulmage@user/Wygulmage) (Ping timeout: 240 seconds) |
| 2026-03-12 20:10:19 +0100 | <ski> | "I was expecting to see - defined using ?< and ?< defined using - xD" -- you could have that for some other pair of alternative operations, i suppose |
| 2026-03-12 20:10:02 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:09:38 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:09:19 +0100 | <ski> | (i also used `|' above to separate alternative definitions, largely for suggestive effect. one could dispense with this use of it, letting the system infer which defining equations together are total on the given inputs) |
| 2026-03-12 20:09:06 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:08:20 +0100 | <ski> | just like `_' is the neutral element of the `&' conjunctive pattern (generalization of `@' where both sides are allowed to be arbitrary patterns. e.g. useful with view patterns, pattern synonyms) |
| 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 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:05:58 +0100 | Wygulmage | (~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 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:05:22 +0100 | AlexNoo__ | (~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 +0100 | AlexNoo | (~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 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:04:08 +0100 | <ski> | is the implementation |