爲什麼不使用Elem typecheck？

Question

我很困惑。

module Experiment 

import Data.Vect 

p1: Elem 5 [3,4,5,6] 
p1 = There (There Here) 

v : Vect 4 Int 
v = 3 :: 4 :: 5 :: 6 :: Nil 

p2: Elem 5 v 
p2 = There (There Here) 

的p2的定義不進行類型檢查，而p1的定義一樣。我正在使用Idris 0.10.2。有什麼我失蹤？

Answer 1

類型聲明中的小寫字母名稱被解釋爲隱式參數（如a在length : List a -> Nat其實際爲length : {a : Type} -> List a -> Nat）。要引用定義的Vect，您可以使用大寫名稱或引用命名空間：

module Experiment 

import Data.Vect 

A : Vect 4 Int 
A = 3 :: 4 :: 5 :: 6 :: Nil 

p2: Elem 5 A 
p2 = There (There Here) 

a : Vect 4 Int 
a = 3 :: 4 :: 5 :: 6 :: Nil 

p3: Elem 5 Experiment.a 
p3 = There (There Here)