clean imports of Precond
authorHelmut Grohne <helmut@subdivi.de>
Thu, 10 Jan 2013 12:16:42 +0000 (13:16 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Thu, 10 Jan 2013 12:16:42 +0000 (13:16 +0100)
Precond.agda

index 3278867..422071c 100644 (file)
@@ -2,15 +2,14 @@ open import Relation.Binary.Core using (Decidable ; _≡_)
 
 module Precond (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where
 
-open import Data.Nat using (ℕ) renaming (zero to nzero ; suc to nsuc)
-open import Data.Fin using (Fin ; zero ; suc)
+open import Data.Nat using (ℕ)
+open import Data.Fin using (Fin)
 open import Data.Vec using (Vec ; [] ; _∷_ ; map ; lookup ; toList)
-open import Data.List.Any using (here ; there)
+import Data.List.Any
 open Data.List.Any.Membership-≡ using (_∉_)
 open import Data.Maybe using (just)
 open import Data.Product using (∃ ; _,_)
 open import Function using (flip ; _∘_)
-open import Relation.Binary.Core using (_≢_)
 open import Relation.Binary.PropositionalEquality using (refl ; cong)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)