It makes you long for a dependently typed language where you really and truly can switch on decidable relations like "compare". For example, I have some Agda c

It makes you long for a dependently typed language where you really and truly can switch on decidable relations like "compare". For example, I have some Agda code (totally unreadable to anyone who didn't write it, i.e. anyone who isn't me) where I switch on whether a+1 is less than, equal to, or greater than x+1, as part of the inductive step in an implementation of the division algorithm, rendering a number into a quotient and a remainder on division by another number. The type system guarantees that I haven't missed any cases. (https://github.com/Smaug123/agdaproofs/blob/9e22ba78f5446ce7272ee342affdfafa2ae189ae/PrimeNumbers.agda#L76 https://github.com/Smaug123/agdaproofs/blob/9e22ba78f5446ce7...)