이드리스 - 평등 주장은 구현이 그와 관련이없는 경우에도,

Question

는 다음과 같은 기능을 고려하시기 바랍니다 실패 : 나는 REPL에서 vectTranspose을 계산하려고하면 예상대로

vectTranspose : Vect n (Fin 3) -> Vect 3 (List (Fin n)) 
vectTranspose {n = Z} [] = [[],[],[]] 
vectTranspose {n = (S len)} (x :: xs) with (natToFin len (S len)) 
    | Just l = let 
     previous = map (map weaken) (vectTranspose xs) 
    in updateAt x (l ::) previous 

, 나는 [[],[],[]]를 얻을.

When checking right hand side of emptyTest with expected type 
     vectTranspose [] = [[], [], []] 

Type mismatch between 
     [[], [], []] = [[], [], []] (Type of Refl) 
and 
     vectTranspose [] = [[], [], []] (Expected type) 

Specifically: 
     Type mismatch between 
       [[], [], []] 
     and 
       vectTranspose [] 

내가 뭔가를 놓치고 있습니까 : 나는 내 코드에서 다음과 같이 동등 주장을 추가하는 경우

여전히

emptyTest : vectTranspose [] = [[],[],[]] 
emptyTest = Refl 

는 내가 컴파일 오류가? 어떻게 든 어썰트에 [[],[],[]]의 유형을 지정해야합니까? 이드리스는

Specifically: 
    Type mismatch between 
      [[], [], []] 
    and 
      vectTranspose [] 

의 유형에 대해 불평하는 것이

Answer 1

사실은 vectTranspose이 유형에 여전히하고 해결되지 않았 음을 나타냅니다. 즉 vectTranspose 총 아니며 실제로 그렇지 않은 경우의 경우 :

당신은 모든 Maybe가지 경우를 포함하지 않았기 때문에 발생

VecTest.vectTranspose is possibly not total due to: 
with block in VecTest.vectTranspose, which is not total as there are missing cases 

.

간단한 해결책은 작은 도우미 함수를 만들 수 :

total 
natToFin': (n: Nat) -> Fin (S n) 
natToFin' Z = FZ 
natToFin' (S k) = FS (natToFin' k) 

total 
vectTranspose : Vect n (Fin 3) -> Vect 3 (List (Fin n)) 
vectTranspose {n = Z} [] = [[], [], []] 
vectTranspose {n = (S len)} (x :: xs) with (natToFin' len) 
    vectTranspose {n = (S len)} (x :: xs) | l = let 
      previous = map (map weaken) (vectTranspose xs) 
      in updateAt x (l ::) previous