Vect n Nat's Evenlyの合計が5になるかどうかを判定しますか？

Question

Cactus私の質問に対処する方法を示しました：Helper Function to Determine if Nat `mod` 5 == 0。

彼が書いた：

onlyModBy5 : (n : Nat) -> {auto prf : n `modNat` 5 = 0} -> Nat 
onlyModBy5 n = n 

をその後、私はVect n Nat年代の合計にonlyModBy5を適用するには、その関数を使用しようとしました。

foo : (n : Nat) -> Vect n Nat -> Nat 
foo n xs = onlyModBy5 $ sum xs 

しかし、私はこのコンパイル時のエラーを得た：

When checking right hand side of foo with expected type 
     Nat 

When checking argument prf to function Main.onlyModBy5: 
     Can't find a value of type 
       Prelude.Nat.modNatNZ, mod' (foldrImpl (\meth => 
                 \meth => 
                  plus meth meth) 
                 0 
                 id 
                 xs) 
              4 
              SIsNotZ 
              (foldrImpl (\meth => 
                 \meth => 
                  plus meth meth) 
                 0 
                 id 
                 xs) 
              (foldrImpl (\meth => 
                 \meth => 
                  plus meth meth) 
                 0 
                 id 
                 xs) 
              4 = 
       0 
Holes: Main.foo 

にはどうすればfooで上記onlyModBy5機能を使用することができますか？

Answer 1

これは達成したいことによって異なります。 foo : (n : Nat) -> Vect n Nat -> Natあなたがfooに任意のNatを適用できることを述べている、とNatのいずれかのVect（Vectサイズnの場合）とfooはNatを返します。

最初に、明示的な(n : Nat)引数は必要ありません。 foo : Vect n Nat -> Natと書くと、Idrisはnを内部的に暗黙の引数：foo : {n : Nat} -> Vect n Nat -> Natに変換します。

Vectの要素についての議論では何もないので、sumについては何もしていません。 [1,2,2]も同様に[1,1]を適用することができますが、後者はprf : (sum [1,1])`modNat`5 == 0)の証明がないため、合計をonlyModBy5に適用することはできません。

あなたは以前のように、引数としての証明を要求することができ、次のいずれか

bar : (xs : Vect n Nat) -> {auto prf : (sum xs) `modNat` 5 = 0} -> Nat 
bar xs = onlyModBy5 (sum xs) 

それとも合計に基づいて決めさせ：

foo : Vect n Nat -> Maybe Nat 
foo xs = foo' (sum xs) 
    where 
    foo' : Nat -> Maybe Nat 
    foo' k with (decEq (k `modNat` 5) 0) 
     | Yes prf = Just (onlyModBy5 k {prf}) 
     | No _ = Nothing 

decEqは（二つの値がpropositionally等しいかどうかを決定しますこの場合は同じNat）、Yesの場合は(prf : n`modNat`5 = 0)、等しい場合はNoは、それらが等しくないという証拠を持っています。この証明はonlyModBy5に{prf}とすることができます。これは{prf=prf}に拡張され、暗黙の引数にという名前のYesという証明が与えられます。