From 0a1558b7cb0bccbe4a8c8411ac08d11a87547eea Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Fri, 7 Feb 2014 18:55:23 +0100 Subject: eliminate useless withs --- FinMap.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'FinMap.agda') diff --git a/FinMap.agda b/FinMap.agda index ce76f18..c46e637 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -103,8 +103,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) -- cgit v1.2.3