Есть ли функция по модулю в idris?

В Prelude.Nat есть

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

Первый требует доказательства того, что делитель не равен нулю, а второй является частичным (т.е. может падать во время выполнения). Практически есть и доказательство,

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

что преемник не может быть нулем. Таким образом, вы можете просто использовать modNatNZ 10 3 SIsNotZ, и система унификации подтвердит Not (3 = 0). Вы можете увидеть, как работает modNatNZ здесь . Поскольку Nat всегда положительное значение, функция остатка будет вести себя так же.

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