3
私は、イドリスで簡単な依存ペアのSemigroup
インターフェイスを実装しようとしている中に依存ペアのための半群が、これはコンパイルされません:エラー実装イドリス
Type mismatch between
ty
and
Nat
と
Semigroup (n ** Vect n f) where
(<+>) (_ ** xs) (_ ** ys) = (_ ** xs ++ ys)
しかし、このコンパイル:
myPair:Type -> Type
myPair f = (n ** Vect n f)
Semigroup (myPair f) where
(<+>) (_ ** xs) (_ ** ys) = (_ ** xs ++ ys)
なぜですか?これを達成する最良の方法は何ですか?