diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-01-28 09:30:45 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-01-28 09:30:45 +0100 |
| commit | f767ec96fec169907da5cb5029852732cf333e7b (patch) | |
| tree | 4844591ccb644defdf054949de5e87078fd0c3a6 /FinMap.agda | |
| parent | 8cc43c2c7e5ab40394a1e6a23470edb3d2d6b909 (diff) | |
| download | bidiragda-f767ec96fec169907da5cb5029852732cf333e7b.tar.gz | |
use the indexed version of the Vec Setoid
Diffstat (limited to 'FinMap.agda')
| -rw-r--r-- | FinMap.agda | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/FinMap.agda b/FinMap.agda index c04c510..ea4f49b 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -19,7 +19,7 @@ open import Relation.Binary.Core using (_≡_ ; refl ; _≢_) open import Relation.Binary.PropositionalEquality using (cong ; sym ; _≗_ ; trans ; cong₂) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) -open import Generic using (just-injective ; vecIsSetoid) +open import Generic using (just-injective) FinMapMaybe : ℕ → Set → Set FinMapMaybe n A = Vec (Maybe A) n |