From: Helmut Grohne Date: Tue, 28 Jan 2014 08:16:26 +0000 (+0100) Subject: cleanup unused function and import X-Git-Url: https://git.linta.de/?p=~helmut%2Fbidiragda.git;a=commitdiff_plain;h=8cc43c2c7e5ab40394a1e6a23470edb3d2d6b909;hp=09cf8a92e03a4cebffdf9bb58aaf1b01b55e73a3;ds=sidebyside cleanup unused function and import --- 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 ()