2 ms·
Though if you allow duplicates, that should be non-decreasing order instead of increasing order?
by jdmichal 5y ago
Though if you allow duplicates, that should be non-decreasing order instead of increasing order?
- didibus 5y agoI think the argument of OP would be that this wouldn't be a bug, because Idris has proved increasing order, which means that if the function allowed duplicate that could result in non-increasing order Idris type checker would have told you your function is incorrect. Basically, the proof is the spec, and a bug is defined as "not behaving as defined by the spec". And assuming Idris is itself bug free in its language implementation and type checker implementation and is powerful enough to prove your given spec, then OP says your function is guaranteed bug free. The difference is that he defines bug as: > When the function behaves outside what Idris has proven. While I think most people define a bug as: > Doesn't do what it should have to provide the correct intended user behavior.