From 2759f0dd1c48bc2976ce5be55ee10c9f0660da6d Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Fri, 16 Mar 2012 11:41:44 +0100
Subject: fix wrong function name in lemma-2

lookup and lookupM reference the same function, but serve different
purposes.
---
 Bidir.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Bidir.agda')

diff --git a/Bidir.agda b/Bidir.agda
index 940a02d..163714a 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -80,7 +80,7 @@ lemma-2 eq (i ∷ is) (x ∷ xs) h () | nothing | _
 lemma-2 eq (i ∷ is) (x ∷ xs) h p | just h' | Reveal_is_.[_] ir = begin
   map (flip lookupM h) (i ∷ is)
     ≡⟨ refl ⟩
-  lookup i h ∷ map (flip lookupM h) is
+  lookupM i h ∷ map (flip lookupM h) is
     ≡⟨ cong (flip _∷_ (map (flip lookup h) is)) (lemma-lookupM-assoc eq i is x xs h (begin
       assoc eq (i ∷ is) (x ∷ xs)
         ≡⟨ cong (flip _>>=_ (checkInsert eq i x)) ir ⟩
-- 
cgit v1.2.3