From f767ec96fec169907da5cb5029852732cf333e7b Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Tue, 28 Jan 2014 09:30:45 +0100
Subject: use the indexed version of the Vec Setoid

---
 Generic.agda | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'Generic.agda')

diff --git a/Generic.agda b/Generic.agda
index f543256..d757c95 100644
--- a/Generic.agda
+++ b/Generic.agda
@@ -76,8 +76,8 @@ toList-subst : {A : Set} → {n m : ℕ} (v : Vec A n) → (p : n ≡ m) →
                toList (subst (Vec A) p v) ≡ toList v
 toList-subst v refl = refl
 
-vecIsISetoid : Setoid ℓ₀ ℓ₀ → ISetoid ℕ ℓ₀ ℓ₀
-vecIsISetoid S = record
+VecISetoid : Setoid ℓ₀ ℓ₀ → ISetoid ℕ ℓ₀ ℓ₀
+VecISetoid S = record
   { Carrier = Vec (Setoid.Carrier S)
   ; _≈_ = λ x → S VecEq.≈ x
   ; isEquivalence = record
@@ -85,7 +85,3 @@ vecIsISetoid S = record
     ; sym = VecEq.sym S
     ; trans = VecEq.trans S }
   }
-
-
-vecIsSetoid : Setoid ℓ₀ ℓ₀ → ℕ → Setoid ℓ₀ ℓ₀
-vecIsSetoid S n = (vecIsISetoid S) at n
-- 
cgit v1.2.3