イドリス - 平等の主張は

Question

を失敗した実装はその関連性がない場合でも、次の関数を考えてみてください：

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 

私はREPLでvectTransposeを計算しようとした場合、予想通り、私は[[],[],[]]を取得します。私は自分のコードに次の

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

のような平等のアサーションを追加する場合

はまだ、私はコンパイルエラーを取得：

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 [] 

私は何かが足りないのですか？私はアサーションの中に何らかの形で[[],[],[]]の型を指定すべきですか？

Answer 1

イドリスは

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

のタイプについて不平を言うということは、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