diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2019-03-31 22:36:21 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2019-03-31 22:36:21 +0200 |
| commit | 8435606d98e418394edbe5104b3f425e56a5a207 (patch) | |
| tree | 49f2d9f5a9066d81f1f5ad59b7e2839510828c2e /Generic.agda | |
| parent | 4071a4a9d85c7187b3a6d324e787adbe282817c0 (diff) | |
| download | bidiragda-8435606d98e418394edbe5104b3f425e56a5a207.tar.gz | |
Generic.toList-fromList is Data.Vec.Properties.toList∘fromList
Diffstat (limited to 'Generic.agda')
| -rw-r--r-- | Generic.agda | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/Generic.agda b/Generic.agda index 3106c5f..323688a 100644 --- a/Generic.agda +++ b/Generic.agda @@ -58,10 +58,6 @@ subst-subst : {A : Set} (T : A → Set) {a b c : A} → (p : a ≡ b) → (p′ P.subst T p′ (P.subst T p x) ≡ P.subst T (P.trans p p′) x subst-subst T P.refl p′ x = P.refl -toList-fromList : {A : Set} → (l : List A) → toList (fromList l) ≡ l -toList-fromList []L = P.refl -toList-fromList (x ∷L xs) = P.cong (_∷L_ x) (toList-fromList xs) - toList-subst : {A : Set} → {n m : ℕ} (v : Vec A n) → (p : n ≡ m) → toList (P.subst (Vec A) p v) ≡ toList v toList-subst v P.refl = P.refl |