Why is Prelude.mod
marked as a total function when it is not defined when the second argument is zero?
<code>Main> :total mod
Prelude.Num.mod is total
</code>
<code>Main> :total mod
Prelude.Num.mod is total
</code>
Main> :total mod
Prelude.Num.mod is total
I was just bit by this and ran into a run-time error, even though Idris2 assured me my functions were total.