Is there a modulo function in idris?

Question

In Haskell, there are the mod and rem functions. Are there similar functions in Idris, particularly defined over Nat?

Answer 1

In Prelude.Nat there are

modNatNZ : Nat -> (y : Nat) -> Not (y = 0) -> Nat
modNat   : Nat -> Nat -> Nat

The first one needs a proof that the divisor is not zero, while the second is partial (i. e. can crash during runtime). Practically there is also a proof,

SIsNotZ : {x: Nat} -> Not (S x = Z)

that a successor cannot be zero. So you can just use modNatNZ 10 3 SIsNotZ and the unification system will proof Not (3 = 0). You can see how modNatNZ works here. As Nat is always positive, a remainder function would behave the same.

Otherwise, a generic

mod : Integral ty => ty -> ty -> ty

is defined for all types implementing Integral (e.g. Int).