idris是否有模函數？

Question

在Haskell中，有mod和rem函數。 Idris中是否有類似的功能，特別是Nat？

Answer 1

在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如何工作here。由於Nat總是正數，所以餘數函數表現相同。

否則，通用

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

被用於實現積分（例如強度）所有類型的定義。