@edwinbrady why does length [1..3] `div` 0 evaluate to 4 : Nat in Idris (0.9.9)?
@sum3rman Nat.div appears to do something odd in the division by zero case. Not sure it should be in the library actually (in that form).
-
-
@edwinbrady according the to sources Nat.div explicitly handles this as (S left). But why? Why this function is declared as total at all? -
@sum3rman It is total as defined. As for why it does that, you'd have to find its author...
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.