length-replicate is now upstream as well
authorHelmut Grohne <helmut@subdivi.de>
Tue, 2 Jan 2018 04:33:53 +0000 (05:33 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Tue, 2 Jan 2018 04:39:00 +0000 (05:39 +0100)
Generic.agda
LiftGet.agda

index 9f1172d..fab3a25 100644 (file)
@@ -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)
index 6849a1a..35bafb1 100644 (file)
@@ -4,7 +4,7 @@ open import Data.Unit using (⊤ ; tt)
 open import Data.Nat using (ℕ ; suc)
 open import Data.Vec using (Vec ; toList ; fromList) renaming ([] to []V ; _∷_ to _∷V_ ; map to mapV)
 open import Data.List using (List ; [] ; _∷_ ; length ; replicate ; map)
-open import Data.List.Properties using (length-map)
+open import Data.List.Properties using (length-map ; length-replicate)
 open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂)
 open import Function using (_∘_ ; flip ; const)
 open import Relation.Binary.Core using (_≡_)
@@ -12,7 +12,7 @@ open import Relation.Binary.PropositionalEquality using (_≗_ ; sym ; cong ; re
 open import Relation.Binary.HeterogeneousEquality as H using (module ≅-Reasoning ; _≅_ ; ≅-to-≡ ; ≡-to-≅ ; ≡-subst-removable) renaming (refl to het-refl ; sym to het-sym ; cong to het-cong ; reflexive to het-reflexive)
 
 import FreeTheorems
-open import Generic using (length-replicate ; toList-fromList ; toList-subst)
+open import Generic using (toList-fromList ; toList-subst)
 open FreeTheorems.ListList using (get-type) renaming (free-theorem to free-theoremL ; Get to GetL ; module Get to GetL)
 open FreeTheorems.VecVec using () renaming (get-type to getV-type ; Get to GetV ; module Get to GetV)