From f767ec96fec169907da5cb5029852732cf333e7b Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Tue, 28 Jan 2014 09:30:45 +0100 Subject: use the indexed version of the Vec Setoid --- FinMap.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'FinMap.agda') 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 -- cgit v1.2.3