diff options
Diffstat (limited to 'Precond.agda')
| -rw-r--r-- | Precond.agda | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/Precond.agda b/Precond.agda index 3278867..422071c 100644 --- a/Precond.agda +++ b/Precond.agda @@ -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_ ; _≡⟨_⟩_ ; _∎) |