Merge branch 'using-vec'
authorHelmut Grohne <helmut@subdivi.de>
Tue, 18 Sep 2012 07:28:00 +0000 (09:28 +0200)
committerHelmut Grohne <helmut@subdivi.de>
Tue, 18 Sep 2012 07:28:00 +0000 (09:28 +0200)
Conflict in Bidir.agda:
  master removed a with i \=? j and using-vec reduced cases that became
  absurd during Vec transformation.

1  2 
Bidir.agda

diff --cc Bidir.agda
@@@ -66,11 -65,11 +65,9 @@@ lemma-∉-lookupM-assoc eq i [
    lookupM i empty
      ≡⟨ lemma-lookupM-empty i ⟩
    nothing ∎
- lemma-∉-lookupM-assoc eq i []         (x' ∷ xs') h () i∉is
- lemma-∉-lookupM-assoc eq i (i' ∷ is') []         h () i∉is
 -lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h ph i∉is with i ≟ i'
 -lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h ph i∉is | yes p = contradiction (here p) i∉is
 -lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h ph i∉is | no ¬p with assoc eq is' xs' | inspect (assoc eq is') xs'
 -lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h () i∉is | no ¬p | nothing | Reveal_is_.[_] ph'
 -lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h ph i∉is | no ¬p | just h' | Reveal_is_.[_] ph' = apply-checkInsertProof eq i' x' h' record {
 +lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h ph i∉is with assoc eq is' xs' | inspect (assoc eq is') xs'
 +lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h () i∉is | nothing | Reveal_is_.[_] ph'
 +lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h ph i∉is | just h' | Reveal_is_.[_] ph' = apply-checkInsertProof eq i' x' h' record {
      same = λ lookupM-i'-h'≡just-x' → begin
        lookupM i h
          ≡⟨ cong (lookupM i) (lemma-from-just (trans (sym ph) (lemma-checkInsert-same eq i' x' h' lookupM-i'-h'≡just-x'))) ⟩