diff options
Diffstat (limited to 'FinMap.agda')
| -rw-r--r-- | FinMap.agda | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/FinMap.agda b/FinMap.agda index 0df0d6f..6342fc5 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -2,7 +2,7 @@ module FinMap where open import Level using () renaming (zero to ℓ₀) open import Data.Nat using (ℕ ; zero ; suc) -open import Data.Maybe using (Maybe ; just ; nothing ; maybe′) +open import Data.Maybe using (Maybe ; just ; nothing ; maybe′ ; just-injective) open import Data.Fin using (Fin ; zero ; suc) open import Data.Fin.Properties using (_≟_) open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr ; zip ; toList) renaming (lookup to lookupVec ; map to mapV) @@ -21,8 +21,6 @@ open import Relation.Binary.Core using (Decidable) open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≢_ ; _≗_) open P.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) -open import Generic using (just-injective) - _∈_ : {A : Set} {n : ℕ} → A → Vec A n → Set _∈_ {A} x xs = Data.List.Membership.Setoid._∈_ (P.setoid A) x (toList xs) |