From 1286deef698a9fbf92b86d0078fd62c47f980ee9 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Sat, 1 Aug 2020 09:12:17 +0200 Subject: move imports for agda-stdlib 1.3 --- Generic.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Generic.agda') diff --git a/Generic.agda b/Generic.agda index ed9d4a4..bac09d8 100644 --- a/Generic.agda +++ b/Generic.agda @@ -9,7 +9,7 @@ open import Data.Maybe.Relation.Binary.Pointwise using (just ; nothing) renaming open import Data.Nat using (ℕ ; zero ; suc) open import Data.Product using (_×_ ; _,_) open import Data.Vec using (Vec ; toList ; fromList ; map) renaming ([] to []V ; _∷_ to _∷V_) -import Data.Vec.Relation.Pointwise.Inductive as VecEq +import Data.Vec.Relation.Binary.Pointwise.Inductive as VecEq open import Data.Vec.Properties using (map-cong) open import Function using (_∘_ ; id ; flip) open import Function.Equality using (_⟶_) -- cgit v1.2.3