vec-len-via-list and length-toList are the same
authorHelmut Grohne <helmut@subdivi.de>
Fri, 14 Sep 2012 15:23:58 +0000 (17:23 +0200)
committerHelmut Grohne <helmut@subdivi.de>
Fri, 14 Sep 2012 15:23:58 +0000 (17:23 +0200)
LiftGet.agda

index c3c5294..d4e7d9f 100644 (file)
@@ -105,10 +105,6 @@ get-trafo-1 get {B} l = begin
 vec-len : {A : Set} {n : ℕ} → Vec A n → ℕ
 vec-len {_} {n} _ = n
 
-vec-len-via-list : {A : Set} {n : ℕ} → (v : Vec A n) → length (toList v) ≡ vec-len v
-vec-len-via-list []V       = refl
-vec-len-via-list (x ∷V xs) = cong suc (vec-len-via-list xs)
-
 length-replicate : {A : Set} {a : A} → (n : ℕ) → length (replicate n a) ≡ n
 length-replicate 0       = refl
 length-replicate (suc n) = cong suc (length-replicate n)
@@ -145,7 +141,7 @@ get-trafo-2-getlen getlen get n = begin
   proj₁ (getList-to-getVec (getVec-to-getList get)) n
     ≡⟨ refl ⟩
   length (toList (get (fromList (replicate n tt))))
-    ≡⟨ vec-len-via-list (get (fromList (replicate n tt))) ⟩
+    ≡⟨ length-toList (get (fromList (replicate n tt))) ⟩
   vec-len (get (fromList (replicate n tt)))
     ≡⟨ cong getlen (length-replicate n) ⟩
   getlen n ∎