From 8546a8812a4fdaf3e3d7a7ba3433894db8b25a14 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Wed, 26 Sep 2012 22:02:48 +0200 Subject: use _\==n_ and _\notin_ instead of \neg Consistent. Shorter. --- Bidir.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Bidir.agda') diff --git a/Bidir.agda b/Bidir.agda index 721b2b2..0720970 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -13,7 +13,7 @@ open import Data.Vec.Properties using (tabulate-∘ ; lookup∘tabulate ; map-co open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂) open import Data.Empty using (⊥-elim) open import Function using (id ; _∘_ ; flip) -open import Relation.Nullary using (yes ; no ; ¬_) +open import Relation.Nullary using (yes ; no) open import Relation.Nullary.Negation using (contradiction) open import Relation.Binary.Core using (_≡_ ; refl) open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; _≗_ ; trans) @@ -104,7 +104,7 @@ lemma-assoc-domain eq (i' ∷ is') (x' ∷ xs') h ph | just h' | [ ph' ] = apply ; wrong = λ x'' x'≢x'' lookupM-i'-h'≡just-x'' → lemma-just≢nothing (trans (sym ph) (lemma-checkInsert-wrong eq i' x' h' x'' x'≢x'' lookupM-i'-h'≡just-x'')) } -lemma-map-lookupM-insert : {m n : ℕ} {A : Set} → (eq : EqInst A) → (i : Fin n) → (is : Vec (Fin n) m) → (x : A) → (h : FinMapMaybe n A) → ¬(i ∈ (toList is)) → (toList is) in-domain-of h → map (flip lookupM (insert i x h)) is ≡ map (flip lookupM h) is +lemma-map-lookupM-insert : {m n : ℕ} {A : Set} → (eq : EqInst A) → (i : Fin n) → (is : Vec (Fin n) m) → (x : A) → (h : FinMapMaybe n A) → i ∉ (toList is) → (toList is) in-domain-of h → map (flip lookupM (insert i x h)) is ≡ map (flip lookupM h) is lemma-map-lookupM-insert eq i [] x h i∉is ph = refl lemma-map-lookupM-insert eq i (i' ∷ is') x h i∉is ph = begin lookupM i' (insert i x h) ∷ map (flip lookupM (insert i x h)) is' -- cgit v1.2.3