From 95609983219f14e8f4c0758cd0688b984d8b1455 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Wed, 5 Feb 2014 15:59:06 +0100
Subject: be more precise about which lookups we use

---
 BFF.agda     |  2 +-
 Bidir.agda   |  4 ++--
 Precond.agda | 10 +++++-----
 3 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/BFF.agda b/BFF.agda
index ddf2307..1770b5e 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -40,4 +40,4 @@ module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
                     g′ = delete-many t′ g
                     h  = assoc t′ v
                     h′ = (flip union g′) <$> h
-                in h′ >>= flip mapMV s′ ∘ flip lookupV
+                in h′ >>= flip mapMV s′ ∘ flip lookupM
diff --git a/Bidir.agda b/Bidir.agda
index fae3b9e..8998ec4 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -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
diff --git a/Precond.agda b/Precond.agda
index 312fbde..354e5f1 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -43,11 +43,11 @@ lemma-union-delete-fromFunc : {m n : ℕ} {A : Set} {is : Vec (Fin n) m} {h : Fi
 lemma-union-delete-fromFunc {is = []} {h = h} {g = g} p = _ , (begin
   union h (fromFunc g)
     ≡⟨ lemma-tabulate-∘ (λ f → begin
-      maybe′ just (lookup f (fromFunc g)) (lookup f h)
-        ≡⟨ cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-fromFunc g f) ⟩
-      maybe′ just (just (g f)) (lookup f h)
-        ≡⟨ lemma-maybe-just (g f) (lookup f h) ⟩
-      just (maybe′ id (g f) (lookup f h)) ∎) ⟩
+      maybe′ just (lookupM f (fromFunc g)) (lookupM f h)
+        ≡⟨ cong (flip (maybe′ just) (lookupM f h)) (lemma-lookupM-fromFunc g f) ⟩
+      maybe′ just (just (g f)) (lookupM f h)
+        ≡⟨ lemma-maybe-just (g f) (lookupM f h) ⟩
+      just (maybe′ id (g f) (lookupM f h)) ∎) ⟩
   tabulate (λ f → just (maybe′ id (g f) (lookup f h)))
     ≡⟨ tabulate-∘ just (λ f → maybe′ id (g f) (lookup f h)) ⟩
   map just (tabulate (λ f → maybe′ id (g f) (lookup f h))) ∎)
-- 
cgit v1.2.3