idris - 如何在向量长度上说服 Idris

Question

刚开始使用 Idris（如果重要的话，那就是 Idris 2），然后偶然发现了这个问题。我正在尝试实现一个函数，该函数返回一个由所有斐波那契数组成的向量，直到给定 n。这是到目前为止的定义（它不编译）：

fibs : (n : Nat) -> Vect (n + 1) Int
fibs Z = [0]
fibs (S Z) = [0, 1]
fibs (S k) =
    case (fibs k) of
        (x :: y :: xs) => (x + y) :: x :: y :: xs

我得到的错误如下：

Can't solve constraint between:
    S (S ?len)
and
    plus ?_ (fromInteger 1)

错误指向表达式(x :: y :: xs)。

我知道我需要向 Idris 证明长度fibs k至少为 2，但我不明白如何做到这一点，以及为什么从现有定义中不明显。对我来说，看起来kinfibs (S k)肯定是 >= 1，否则要么匹配fibs Z要么fibs (S Z)匹配。fibs k因此，根据 的定义， where的长度k >= 1必须 >= 2 fibs : (n : Nat) -> Vect (n + 1) Int。我错过了什么以及如何在 Idris 中表达这一点？

Answer 1