
12 Jan
2023
12 Jan
'23
12:24 p.m.
Hey! 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. https://www.youtube.com/watch?v=PHS3Q-tRjFQ https://www.youtube.com/watch?v=WHeBxSBY0fc https://www.youtube.com/watch?v=dK5be4cdQdE https://www.youtube.com/watch?v=8AKtqFY1ueM https://www.youtube.com/watch?v=jPZciAJ0oaw https://www.youtube.com/watch?v=S5Oz_w9HDs0 Hope that helps Dan Dart