3 ms·

That's exactly what my framework does. As long as you're okay with runtime panics (which would happen anyway in a non-dependently typed language), you just have

That's exactly what my framework does. As long as you're okay with runtime panics (which would happen anyway in a non-dependently typed language), you just have any function you don't know how to prove go from SortedList -> List. Then you have a check List -> Maybe SortedList. And finally a function with a panic that lets you write the SortedList -> SortedList version.

nerdponx 4y ago
> a function with a panic that lets you write the SortedList -> SortedList Ah, I think I see what you mean. Yes, that's also possible, but you are losing the full safety of dependent types, and are just back to contracts!