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. --- Bidir.agda | 3 --- 1 file changed, 3 deletions(-) (limited to 'Bidir.agda') diff --git a/Bidir.agda b/Bidir.agda index a77a9db..cca2ba7 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -18,9 +18,6 @@ open import Data.Vec.Equality using () renaming (module Equality to VecEq) open import Data.Vec.Properties using (tabulate-∘ ; lookup∘tabulate ; map-cong ; map-∘) open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂) open import Function using (id ; _∘_ ; flip) -open import Function.Equality using (_⟶_ ; _⟨$⟩_) -open import Function.Injection using (module Injection) renaming (Injection to _↪_) -open Injection using (to) open import Relation.Binary.Core using (refl ; _≡_) open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid) open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans ; cong₂ ; decSetoid ; module ≡-Reasoning) renaming (setoid to EqSetoid) -- cgit v1.2.3