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 /Generic.agda | |
| parent | 8cc43c2c7e5ab40394a1e6a23470edb3d2d6b909 (diff) | |
| download | bidiragda-f767ec96fec169907da5cb5029852732cf333e7b.tar.gz | |
use the indexed version of the Vec Setoid
Diffstat (limited to 'Generic.agda')
| -rw-r--r-- | Generic.agda | 8 |
1 files changed, 2 insertions, 6 deletions
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 |