diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-10 15:50:27 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-10 15:50:27 +0100 |
| commit | 6cc566c46889c5e7aafc8d75c6627137e56ab30f (patch) | |
| tree | 092dce779785d17f572dfd1880baa23c69cd1a33 /FinMap.agda | |
| parent | 586d72e18898311d975f5748bca397c403b6a83b (diff) | |
| parent | 04b7bf8fabf64a2414d64cfb385f6a397da0a0fb (diff) | |
| download | bidiragda-6cc566c46889c5e7aafc8d75c6627137e56ab30f.tar.gz | |
Merge branch master into feature-shape-update
For building on the sieve example.
Diffstat (limited to 'FinMap.agda')
| -rw-r--r-- | FinMap.agda | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/FinMap.agda b/FinMap.agda index 34e2fc1..240bbe1 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -108,8 +108,7 @@ lemma-fromFunc-tabulate {zero} f = refl lemma-fromFunc-tabulate {suc _} f = cong (_∷_ (just (f zero))) (lemma-fromFunc-tabulate (f ∘ suc)) lemma-lookupM-delete : {n : ℕ} {A : Set} {i j : Fin n} → (f : FinMapMaybe n A) → i ≢ j → lookupM i (delete j f) ≡ lookupM i f -lemma-lookupM-delete {i = zero} {j = zero} (_ ∷ _) p with p refl -... | () +lemma-lookupM-delete {i = zero} {j = zero} (_ ∷ _) p = contradiction refl p lemma-lookupM-delete {i = zero} {j = suc j} (_ ∷ _) p = refl lemma-lookupM-delete {i = suc i} {j = zero} (x ∷ xs) p = refl lemma-lookupM-delete {i = suc i} {j = suc j} (x ∷ xs) p = lemma-lookupM-delete xs (p ∘ cong suc) |