如何理解Idris lang中List和Vect的类型声明和定义？

Question

在Idris doc中有以下几行：

data List a = Nil | (::) a (List a)

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

我假设第1行是List的类型定义，其余的是Vect的类型声明。我认为应该同时包含声明和定义，因此我查看了Idris repo并发现：

data List : (elem : Type) -> Type where
  Nil : List elem
  (::) : (x : elem) -> (xs : List elem) -> List elem

这与Vect的类型声明具有相似的模式，因此看起来不错。但是我在源代码中找不到data List a = Nil | (::) a (List a)。另外，我找不到Vect的类型定义。

所以，我的困惑是：

• 为什么我在源代码中找不到data List a = Nil | (::) a (List a)？
• Vect的实际类型定义是什么？

Answer 1

在Idris中没有单独的“类型定义”和“类型声明”；这只是编写类型定义的两种方法。参见Syntax Guide：