|
|
|
|
|
|
by klysm
596 days ago
|
|
|
I have no idea what I’m talking about, but it seems like these restricted cases of inequality flow control type checking are very similar in power to dependent types, but don’t require the same level of complexity. It’s nice being able to write imperative proofs of correctness guided by the compiler. |
|
|