From c98062b949a6fc792b042e04453b0bed27941caa Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Tue, 2 Jan 2018 05:33:53 +0100 Subject: length-replicate is now upstream as well --- LiftGet.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'LiftGet.agda') diff --git a/LiftGet.agda b/LiftGet.agda index 6849a1a..35bafb1 100644 --- a/LiftGet.agda +++ b/LiftGet.agda @@ -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) -- cgit v1.2.3