length-replicate is now upstream as well

1 files changed, 1 insertions, 5 deletions

diff --git a/Generic.agda b/Generic.agda
index 9f1172d..fab3a25 100644
--- a/Generic.agda
+++ b/Generic.agda
@@ -2,7 +2,7 @@ module Generic where
 
 import Category.Functor
 import Category.Monad
-open import Data.List using (List ; length ; replicate) renaming ([] to []L ; _∷_ to _∷L_)
+open import Data.List using (List) renaming ([] to []L ; _∷_ to _∷L_)
 open import Data.Maybe using (Maybe ; just ; nothing) renaming (setoid to MaybeEq)
 open import Data.Nat using (ℕ ; zero ; suc)
 open import Data.Product using (_×_ ; _,_)
@@ -27,10 +27,6 @@ open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_)
 just-injective : {A : Set} → {x y : A} → Maybe.just x ≡ Maybe.just y → x ≡ y
 just-injective refl = refl
 
-length-replicate : {A : Set} {a : A} → (n : ℕ) → length (replicate n a) ≡ n
-length-replicate zero    = refl
-length-replicate (suc n) = cong suc (length-replicate n)
-
 sequenceV : {A : Set} {n : ℕ} → Vec (Maybe A) n → Maybe (Vec A n)
 sequenceV []V       = just []V
 sequenceV (x ∷V xs) = x >>= (λ y → (_∷V_ y) <$> sequenceV xs)