From 71025b5f1d0a11b0cf373192210b293a77d45c04 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Mon, 27 Jan 2014 09:31:56 +0100 Subject: cleanup unused functions and useless steps --- Bidir.agda | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) (limited to 'Bidir.agda') diff --git a/Bidir.agda b/Bidir.agda index eef8bff..05ee066 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -22,7 +22,7 @@ open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨ import FreeTheorems open FreeTheorems.VecVec using (get-type ; free-theorem) -open import Generic using (just-injective ; map-just-injective ; mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map) +open import Generic using (just-injective ; mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map) open import FinMap import CheckInsert open CheckInsert Carrier deq @@ -150,14 +150,6 @@ lemma->>=-just : {A B : Set} (ma : Maybe A) {f : A → Maybe B} {b : B} → (ma lemma->>=-just (just a) p = a , refl lemma->>=-just nothing () -lemma-mapMV-just : {A B : Set} {n : ℕ} {f : A → Maybe B} {s : Vec A n} {v : Vec B n} → mapMV f s ≡ just v → All (λ x → ∃ λ y → f x ≡ just y) (toList s) -lemma-mapMV-just {s = []} p = Data.List.All.[] -lemma-mapMV-just {f = f} {s = x ∷ xs} p with f x | inspect f x -lemma-mapMV-just {s = x ∷ xs} () | nothing | _ -lemma-mapMV-just {f = f} {s = x ∷ xs} p | just y | [ py ] with mapMV f xs | inspect (mapMV f) xs -lemma-mapMV-just {s = x ∷ xs} () | just y | [ py ] | nothing | _ -lemma-mapMV-just {s = x ∷ xs} p | just y | [ py ] | just ys | [ pys ] = (y , py) Data.List.All.∷ (lemma-mapMV-just pys) - lemma-just-sequence : {A : Set} {n : ℕ} → (v : Vec A n) → sequenceV (map just v) ≡ just v lemma-just-sequence [] = refl lemma-just-sequence (x ∷ xs) rewrite lemma-just-sequence xs = refl -- cgit v1.2.3