은`decEq`

Question

는 주어의 이해 :

*section3> :module Data.Vect  
*section3> :let e = the (Vect 0 Int) [] 
*section3> :let xs = the (Vect _ _) [1,2] 

*section3> decEq xs e 
(input):1:7:When checking argument x2 to function Decidable.Equality.decEq: 
     Type mismatch between 
       Vect 0 Int (Type of e) 
     and 
       Vect 2 Integer (Expected type) 

     Specifically: 
       Type mismatch between 
         0 
       and 
         2 

왜 Nat 인수 DecEq 서로 동일해야?

주 - https://groups.google.com/forum/#!topic/idris-lang/qgtImCLka3I에 게시 원래

Answer 1

decEq는 균일 명제 평등을위한 것입니다 : 당신이 볼 수 있듯이

||| Decision procedures for propositional equality 
interface DecEq t where 
    ||| Decide whether two elements of `t` are propositionally equal 
    total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2) 

, x1 및 x2 유형 t의 등록 상표입니다. 귀하의 경우에는 x1 : Vect 2 Integer 및 x2 : Vect 0 Int입니다. 이들은 두 가지 유형입니다.

import Data.Vect 

vectLength : {xs : Vect n a} -> {ys : Vect m a} -> xs = ys -> n = m 
vectLength {n = n} {m = n} Refl = Refl 

decEqVect : (DecEq a) => (xs : Vect n a) -> (ys : Vect m a) -> Dec (xs = ys) 
decEqVect {n = n} {m = m} xs ys with (decEq n m) 
decEqVect xs ys | Yes Refl = decEq xs ys 
decEqVect xs ys | No notEq = No (notEq . vectLength)