diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-05 15:59:06 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-05 15:59:06 +0100 |
| commit | 95609983219f14e8f4c0758cd0688b984d8b1455 (patch) | |
| tree | 497e596edcbca0a745d1a42fb1995dc731631dac /Bidir.agda | |
| parent | 5f11a53df7da1df3757cf8fd54652f78a50afbf0 (diff) | |
| download | bidiragda-95609983219f14e8f4c0758cd0688b984d8b1455.tar.gz | |
be more precise about which lookups we use
Diffstat (limited to 'Bidir.agda')
| -rw-r--r-- | Bidir.agda | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -141,7 +141,7 @@ theorem-1 G s = begin ≡⟨ cong (h′↦r ∘ just) (lemma-disjoint-union (denumerate s) (get (enumerate s))) ⟩ (h′↦r ∘ just) (fromFunc (denumerate s)) ≡⟨ refl ⟩ - mapMV (flip lookupVec (fromFunc (denumerate s))) (enumerate s) + mapMV (flip lookupM (fromFunc (denumerate s))) (enumerate s) ≡⟨ mapMV-cong (lemma-lookupM-fromFunc (denumerate s)) (enumerate s) ⟩ mapMV (Maybe.just ∘ denumerate s) (enumerate s) ≡⟨ mapMV-purity (denumerate s) (enumerate s) ⟩ @@ -151,7 +151,7 @@ theorem-1 G s = begin where open ≡-Reasoning open Get G h↦h′ = _<$>_ (flip union (delete-many (get (enumerate s)) (fromFunc (denumerate s)))) - h′↦r = flip _>>=_ (flip mapMV (enumerate s) ∘ flip lookupVec) + h′↦r = flip _>>=_ (flip mapMV (enumerate s) ∘ flip lookupM) lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → f <$> ma ≡ just b → ∃ λ a → ma ≡ just a |