From ad721d4770c02769a9b7afab90160d1818afe1d6 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Tue, 21 Jun 2016 17:50:07 +0200 Subject: fix compilation with agda 2.5.1, agda-stdlib 0.12 --- Bidir.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Bidir.agda b/Bidir.agda index 790f9b9..1022fab 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -144,7 +144,7 @@ theorem-1 G {i} s = begin h′↦r = (λ f′ → fmapS f′ t) ∘ flip lookupM -lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → f <$> ma ≡ just b → ∃ λ a → ma ≡ just a +lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → (f <$> ma) ≡ just b → ∃ λ a → ma ≡ just a lemma-<$>-just (just x) f<$>ma≡just-b = x , refl lemma-<$>-just nothing () @@ -218,7 +218,7 @@ module _ (G : Get) where open Shaped SourceShapeT using () renaming (sequence to sequenceSource) open Shaped ViewShapeT using () renaming (sequence to sequenceView) - lemma-get-sequence : {A : Set} → {i : I} {v : SourceContainer (Maybe A) (gl₁ i)} {r : SourceContainer A (gl₁ i)} → sequenceSource v ≡ just r → get <$> sequenceSource v ≡ sequenceView (get v) + lemma-get-sequence : {A : Set} → {i : I} {v : SourceContainer (Maybe A) (gl₁ i)} {r : SourceContainer A (gl₁ i)} → sequenceSource v ≡ just r → (get <$> sequenceSource v) ≡ sequenceView (get v) lemma-get-sequence {v = v} {r = r} p = begin get <$> sequenceSource v ≡⟨ cong (_<$>_ get ∘ sequenceSource) (lemma-sequence-successful SourceShapeT v p) ⟩ -- cgit v1.2.3