author Helmut Grohne Fri, 7 Feb 2014 17:32:54 +0000 (18:32 +0100) committer Helmut Grohne Fri, 7 Feb 2014 17:32:54 +0000 (18:32 +0100)
 Bidir.agda patch | blob | history Generic.agda patch | blob | history

index 8998ec4..da9cafb 100644 (file)
@@ -176,8 +176,8 @@ lemma->>=-just (just a) p = a , refl
lemma->>=-just nothing  ()

lemma-just-sequence : {A : Set} {n : ℕ} → (v : Vec A n) → sequenceV (map just v) ≡ just v
-lemma-just-sequence [] = refl
-lemma-just-sequence (x ∷ xs) rewrite lemma-just-sequence xs = refl
+lemma-just-sequence []       = refl
+lemma-just-sequence (x ∷ xs) = cong (_<\$>_ (_∷_ x)) (lemma-just-sequence xs)

lemma-mapM-successful : {A B : Set} {f : A → Maybe B} {n : ℕ} → (v : Vec A n) → {r : Vec B n} → mapMV f v ≡ just r → ∃ λ w → map f v ≡ map just w
lemma-mapM-successful         []      p = [] , refl
index 748a49a..b1ab8dd 100644 (file)
@@ -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