12 Jan
2023
12 Jan
'23
12:49 p.m.
On Thu, 12 Jan 2023, Dan Dart wrote:
I had a go at this too the other week and came across the same >= == problem you're having.
I'm not sure if it's doable this way without dependent types, but maybe typed unary would work. I found a good video series to study by Richard A. Eisenberg. He mentions typed unary numbers and goes over existentials such that he doesn't have the same problem.
So far I am using type-level decimal numbers of the 'tfp' package. My numbers can become a bit bigger, like 256 or 512, so Unary might be too slow.