From db1e29ec11c0cc0a874ef9df25b30abca960595d Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Mon, 3 Feb 2014 16:36:11 +0100 Subject: 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 --- Generic.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Generic.agda') 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 -- cgit v1.2.3