diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-04-27 20:53:05 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-04-27 20:53:05 +0200 |
| commit | ddb751df76c004d788ed09c3ed54c562c99afb7b (patch) | |
| tree | 8f99c34cd4f2ad3d8ffc8f64291e5018ac4968a8 | |
| parent | cab5a60cefea9ca03dbdde0a4a33cec20aaeabf6 (diff) | |
| download | bidiragda-ddb751df76c004d788ed09c3ed54c562c99afb7b.tar.gz | |
lemma-2: do not confuse lookup with lookupM
Even though they are the same.
| -rw-r--r-- | Bidir.agda | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -232,7 +232,7 @@ lemma-2 eq (i ∷ is) (x ∷ xs) h p | just h' | Reveal_is_.[_] ir = begin map (flip lookupM h) (i ∷ is) ≡⟨ refl ⟩ 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 + ≡⟨ cong (flip _∷_ (map (flip lookupM 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 ⟩ checkInsert eq i x h' |