|
|
|
|
|
|
by Zalastax
2819 days ago
|
|
|
You could just assert that i%2 == 0 via some postulate - as long as the proof is irrelevant for the code that is. Doing so is similar to converting from any in a gradual type system: if the assertion is correct you get correct code with little work and if you're uncorrect you're no worse off than if you had no types at all. There are difficulties with dependent types, but having to go all in can be avoided via a shift in culture. |
|
|