相关疑难解决方法(0)

" 使用Idris进行类型驱动开发 "一书介绍了此练习:

定义适合签名的可能方法:

two : (xs : Vect n elem) -> Vect (n * 2) elem

我试过了:

two : (xs : Vect n elem) -> Vect (n * 2) elem
two xs = xs ++ xs

但是我收到以下错误:

*One> :r
Type checking ./One.idr
One.idr:9:5:When checking right hand side of two:
Type mismatch between
        Vect (n + n) elem (Type of xs ++ xs)
and
        Vect (mult n 2) elem (Expected type)

Specifically:
        Type mismatch between
                plus n n
        and
                mult …

我正在玩伊德里斯,我遇到了一些令我困惑的事:

以下类型检查:

conc : Vect n a -> Vect m a -> Vect (n+m) a
conc [] ys = ys
conc (x :: xs) ys = x :: (conc xs ys)

但这不是:

conc : Vect n a -> Vect m a -> Vect (m+n) a
conc [] ys = ys
conc (x :: xs) ys = x :: (conc xs ys)

出现以下错误:

When checking right hand side of conc with expected type
        Vect (m + 0) a

Type mismatch between …