diff options
Diffstat (limited to 'LiftGet.agda')
| -rw-r--r-- | LiftGet.agda | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/LiftGet.agda b/LiftGet.agda index c3c5294..d4e7d9f 100644 --- a/LiftGet.agda +++ b/LiftGet.agda @@ -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 ∎ |