diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2013-01-10 11:09:38 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2013-01-10 11:09:38 +0100 |
| commit | d42ffc9d24adb2b416ff73708ae64c1d4ca50c30 (patch) | |
| tree | 48b105cf1f30c79c4a9869d954bdeb9c652e30f2 /Bidir.agda | |
| parent | 400b30320b90620e47a16f3f1ec4ce3dad37e8b0 (diff) | |
| download | bidiragda-d42ffc9d24adb2b416ff73708ae64c1d4ca50c30.tar.gz | |
reduce a precondition of lemma-checkInsert-lookupM
Now it looks a lot more like lemma-lookupM-insert-other, so rename it to
lemma-lookupM-checkInsert-other.
Diffstat (limited to 'Bidir.agda')
| -rw-r--r-- | Bidir.agda | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -62,7 +62,7 @@ lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') h ph i∉is with assoc is' x lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') h () i∉is | nothing | [ ph' ] lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') h ph i∉is | just h' | [ ph' ] = begin lookupM i h - ≡⟨ sym (lemma-checkInsert-lookupM i i' (i∉is ∘ here) x' (lookupVec i h) h' h refl ph) ⟩ + ≡⟨ sym (lemma-lookupM-checkInsert-other i i' (i∉is ∘ here) x' h' h ph) ⟩ lookupM i h' ≡⟨ lemma-∉-lookupM-assoc i is' xs' h' ph' (i∉is ∘ there) ⟩ nothing ∎ |