"There" 在 idris 教程第 11 页第 3.4.4 节中如何工作？

Question

以下是教程中的示例，为简单起见稍作修改：

data Vect : Nat -> (b:Type) -> Type where
  Nil : Vect Z a
  (::) : a -> Vect k a -> Vect (S k) a

data Elem : a -> Vect n a -> Type where
  Here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)
  There : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)

testVec : Vect 4 Int
testVec = 3 :: 4 :: 5 :: 6 :: Nil
inVect : Elem 4 testVec
inVect = There Here

我无法理解 There 如何验证该值是否正确。据我了解， There 就像一个函数一样工作，所以它需要 Here类型的元素，填空时对应Elem 3 testVec，然后将testVec的第一个值设置为y，其余设置为xs.但是由于 y 没有在任何地方使用，所以我希望除此之外不会造成任何限制。

然而，当我尝试

inVectBroken : Elem 2 testVec
inVectBroken = There Here

我得到一个错误：

When checking an application of constructor There:
Type mismatch between
        Elem x (x :: xs) (Type of Here)
and
        Elem 2 [4, 5, 6] (Expected type)

Specifically:
        Type mismatch between
                2
        and
                4

谁能给我解释一下上面的代码是如何（神奇地？）将 There 限制在 Vect 的尾部的？

Answer 1

Here 4 (x :: xs)是4在(x :: xs)开头的证明，所以x = 4。 There 证明 Elem 4 xs 4 在 xs 的某处，因此证明 Elem 4 (y :: xs)，4 仍然在扩展列表的某处。那就是 y 去的地方。 y 实际上是什么并不重要，它只是允许将证明扩展到更大的列表。例如：

in1 : Elem 4 (4 :: Nil)
in1 = Here

in2 : Elem 4 (3 :: 4 :: Nil)
in2 = There in1

in3 : Elem 4 (8 :: 4 :: Nil)
in3 = There in1

根据类型，您可以看到在整个证明中变化的不是元素 4，而是列表。

"There" 在 idris 教程第 11 页第 3.4.4 节中如何工作？

How does "There" work in the idris tutorial, page 11, section 3.4.4?

idris