diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2019-03-31 22:01:56 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2019-03-31 22:01:56 +0200 |
| commit | 4071a4a9d85c7187b3a6d324e787adbe282817c0 (patch) | |
| tree | 76d0530f9d2f7f784cb9b98603066e955b27fc30 /FinMap.agda | |
| parent | e83a3b6cce71c20ffb83475c2660e9500d18798e (diff) | |
| download | bidiragda-4071a4a9d85c7187b3a6d324e787adbe282817c0.tar.gz | |
Generic.just-injective is Data.Maybe.just-injective
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) |