From ce4bbcc0c06b088a10881fcd66da5422571e7995 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Tue, 4 Feb 2014 11:12:42 +0100 Subject: remove unused imports Most of the became unused by using the convenience functions introduced in the parent commit. --- BFF.agda | 4 ---- 1 file changed, 4 deletions(-) (limited to 'BFF.agda') diff --git a/BFF.agda b/BFF.agda index f5573ba..ced6ebf 100644 --- a/BFF.agda +++ b/BFF.agda @@ -11,11 +11,7 @@ open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_) open import Data.List using (List ; [] ; _∷_ ; map ; length) open import Data.Vec using (Vec ; toList ; fromList ; tabulate ; allFin) renaming (lookup to lookupV ; map to mapV ; [] to []V ; _∷_ to _∷V_) open import Function using (id ; _∘_ ; flip) -open import Function.Equality using (_⟶_ ; _⟨$⟩_) -open import Function.Injection using (module Injection) renaming (Injection to _↪_ ; id to id↪) open import Relation.Binary using (Setoid ; DecSetoid ; module DecSetoid) -open import Relation.Binary.PropositionalEquality using (cong) renaming (setoid to EqSetoid) -open Injection using (to) open import FinMap open import Generic using (mapMV ; ≡-to-Π) -- cgit v1.2.3