diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-03 16:36:11 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2014-02-03 16:36:11 +0100 |
| commit | db1e29ec11c0cc0a874ef9df25b30abca960595d (patch) | |
| tree | 3abef25f15ac6067a34eeda7ff8ee823f90a6cbb /Generic.agda | |
| parent | 39bae2aebe94d04b981e006e33fcf96c86acbf56 (diff) | |
| download | bidiragda-db1e29ec11c0cc0a874ef9df25b30abca960595d.tar.gz | |
make things compile with 2.3.0.1
* Remove let patter , match = foo usage
* Remove Qualified.infix-symbol usage
* Add non-obvious absurd patterns
* Qualify constructors
Diffstat (limited to 'Generic.agda')
| -rw-r--r-- | Generic.agda | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Generic.agda b/Generic.agda index 81292ff..748a49a 100644 --- a/Generic.agda +++ b/Generic.agda @@ -36,7 +36,7 @@ mapMV-cong {f = f} {g = g} f≗g (x ∷V xs) with f x | g x | f≗g x mapMV-cong f≗g (x ∷V xs) | just y | .(just y) | refl = cong (_<$>_ (_∷V_ y)) (mapMV-cong f≗g xs) mapMV-cong f≗g (x ∷V xs) | nothing | .nothing | refl = refl -mapMV-purity : {A B : Set} {n : ℕ} → (f : A → B) → (v : Vec A n) → mapMV (just ∘ f) v ≡ just (map f v) +mapMV-purity : {A B : Set} {n : ℕ} → (f : A → B) → (v : Vec A n) → mapMV (Maybe.just ∘ f) v ≡ just (map f v) mapMV-purity f []V = refl mapMV-purity f (x ∷V xs) rewrite mapMV-purity f xs = refl @@ -80,7 +80,7 @@ toList-subst v refl = refl VecISetoid : Setoid ℓ₀ ℓ₀ → ISetoid ℕ ℓ₀ ℓ₀ VecISetoid S = record { Carrier = Vec (Setoid.Carrier S) - ; _≈_ = λ x → S VecEq.≈ x + ; _≈_ = λ x → VecEq._≈_ S x ; isEquivalence = record { refl = VecEq.refl S _ ; sym = VecEq.sym S |