小编sca*_*aza的帖子

以下向量声明 cons

cons : a -> Vect n a -> Vect (n + 1) a
cons x xs = x :: xs

因错误而失败

Type mismatch between
                S n
        and
                plus n 1

而以下矢量append编译和工作

append : Vect n a -> Vect m a -> Vect (n + m) a
append xs ys = xs ++ ys

为什么plus第二种情况接受类型级别,而第一种情况不接受.有什么不同？