diff options
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 748a49a..b1ab8dd 100644 --- a/Generic.agda +++ b/Generic.agda @@ -37,8 +37,8 @@ mapMV-cong f≗g (x ∷V xs) | just y | .(just y) | refl = cong (_<$>_ (_∷V_ y 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 (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 +mapMV-purity f []V = refl +mapMV-purity f (x ∷V xs) = cong (_<$>_ (_∷V_ (f x))) (mapMV-purity f xs) maybeEq-from-≡ : {A : Set} {a b : Maybe A} → a ≡ b → MaybeEq (PropEq A) ∋ a ≈ b maybeEq-from-≡ {a = just x} {b = .(just x)} refl = just refl |