From 1e2ddab6a91377a939d47e30ed1575b03784a09f Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 26 Jan 2012 16:05:23 +0100 Subject: reduce imports to speed up agda-mode --- Bidir.agda | 26 ++++++++++++-------------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/Bidir.agda b/Bidir.agda index 9604e00..0c41319 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -1,18 +1,16 @@ module Bidir where -open import Data.Bool hiding (_≟_) -open import Data.Nat -open import Data.Fin -open import Data.Fin.Props renaming (_≟_ to _≟F_) -open import Data.Maybe -open import Data.List hiding (replicate) -open import Data.Vec hiding (map ; zip ; _>>=_) renaming (lookup to lookupVec) -open import Data.Product hiding (zip ; map) -open import Function -open import Relation.Nullary -open import Relation.Nullary.Negation -open import Relation.Binary.Core -open import Relation.Binary.PropositionalEquality -open Relation.Binary.PropositionalEquality.≡-Reasoning + +open import Data.Nat using (ℕ) +open import Data.Fin using (Fin) +open import Data.Maybe using (Maybe ; nothing ; just ; maybe′) +open import Data.List using (List ; [] ; _∷_ ; map ; length) +open import Data.Vec using (toList ; fromList ; tabulate) renaming (lookup to lookupVec) +open import Function using (id ; _∘_ ; flip) +open import Relation.Nullary using (Dec ; yes ; no) +open import Relation.Nullary.Negation using (contradiction) +open import Relation.Binary.Core using (_≡_ ; refl) +open import Relation.Binary.PropositionalEquality using (cong ; inspect ; Reveal_is_) +open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) open import FinMap -- cgit v1.2.3