diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-07 18:32:54 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-07 18:32:54 +0100 |
| commit | c9ddcf0abbb2e82eafc6dc24872244374c4f43c2 (patch) | |
| tree | 5b43684abd33d60586a5e2827684d51026b9611b /Generic.agda | |
| parent | 95609983219f14e8f4c0758cd0688b984d8b1455 (diff) | |
| download | bidiragda-c9ddcf0abbb2e82eafc6dc24872244374c4f43c2.tar.gz | |
replace rewrite with cong where feasible
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 |