From 8cc43c2c7e5ab40394a1e6a23470edb3d2d6b909 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Tue, 28 Jan 2014 09:16:26 +0100 Subject: [PATCH 1/1] cleanup unused function and import --- Bidir.agda | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/Bidir.agda b/Bidir.agda index 32d0ae7..838df25 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -25,7 +25,7 @@ import Relation.Binary.EqReasoning as EqR import FreeTheorems open FreeTheorems.VecVec using (get-type ; free-theorem) -open import Generic using (just-injective ; vecIsSetoid ; mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map) +open import Generic using (vecIsSetoid ; mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map) open import FinMap import CheckInsert open CheckInsert A @@ -170,10 +170,6 @@ lemma-union-not-used h h' (i ∷ is') (Data.List.All._∷_ (x , px) p') = cong (lemma-union-not-used h h' is' p') where open ≡-Reasoning -map-just-≈-injective : {n : ℕ} {x y : Vec Carrier n} → Setoid._≈_ (vecIsSetoid (MaybeSetoid A.setoid) n) (map just x) (map just y) → Setoid._≈_ (vecIsSetoid A.setoid n) x y -map-just-≈-injective {x = []} {y = []} VecEq.[]-cong = VecEq.[]-cong -map-just-≈-injective {x = _ ∷ _} {y = _ ∷ _} (just x≈y VecEq.∷-cong ps) = x≈y VecEq.∷-cong map-just-≈-injective ps - lemma->>=-just : {A B : Set} (ma : Maybe A) {f : A → Maybe B} {b : B} → (ma >>= f) ≡ just b → ∃ λ a → ma ≡ just a lemma->>=-just (just a) p = a , refl lemma->>=-just nothing () -- 2.20.1