use _\==n_ and _\notin_ instead of \neg

Consistent. Shorter.

3 files changed, 10 insertions, 10 deletions

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'
diff --git a/CheckInsert.agda b/CheckInsert.agda
index c482423..40a57d6 100644
--- a/CheckInsert.agda
+++ b/CheckInsert.agda
@@ -5,9 +5,9 @@ open import Data.Fin using (Fin)
 open import Data.Fin.Props using (_≟_)
 open import Data.Maybe using (Maybe ; nothing ; just)
 open import Data.List using (List ; [] ; _∷_)
-open import Relation.Nullary using (Dec ; yes ; no ; ¬_)
+open import Relation.Nullary using (Dec ; yes ; no)
 open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Binary.Core using (_≡_ ; refl)
+open import Relation.Binary.Core using (_≡_ ; refl ; _≢_)
 open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 
@@ -27,7 +27,7 @@ record checkInsertProof {A : Set} {n : ℕ} (eq : EqInst A) (i : Fin n) (x : A)
   field
      same : lookupM i m ≡ just x → P
      new : lookupM i m ≡ nothing → P
-     wrong : (x' : A) → ¬(x ≡ x') → lookupM i m ≡ just x'  → P
+     wrong : (x' : A) → x ≢ x' → lookupM i m ≡ just x'  → P
 
 apply-checkInsertProof : {A P : Set} {n : ℕ} → (eq : EqInst A) → (i : Fin n) → (x : A) → (m : FinMapMaybe n A) → checkInsertProof eq i x m P → P
 apply-checkInsertProof eq i x m rp with lookupM i m | inspect (lookupM i) m
@@ -46,7 +46,7 @@ lemma-checkInsert-new : {A : Set} {n : ℕ} → (eq : EqInst A) → (i : Fin n)
 lemma-checkInsert-new eq i x m p with lookupM i m
 lemma-checkInsert-new eq i x m refl | .nothing = refl
 
-lemma-checkInsert-wrong : {A : Set} {n : ℕ} → (eq : EqInst A) → (i : Fin n) → (x : A) → (m : FinMapMaybe n A) → (x' : A) → ¬(x ≡ x') → lookupM i m ≡ just x' → checkInsert eq i x m ≡ nothing
+lemma-checkInsert-wrong : {A : Set} {n : ℕ} → (eq : EqInst A) → (i : Fin n) → (x : A) → (m : FinMapMaybe n A) → (x' : A) → x ≢ x' → lookupM i m ≡ just x' → checkInsert eq i x m ≡ nothing
 lemma-checkInsert-wrong eq i x m x' d p with lookupM i m
 lemma-checkInsert-wrong eq i x m x' d refl | .(just x') with eq x x'
 lemma-checkInsert-wrong eq i x m x' d refl | .(just x') | yes q = contradiction q d
@@ -56,7 +56,7 @@ record checkInsertEqualProof {A : Set} {n : ℕ} (eq : EqInst A) (i : Fin n) (x
   field
      same : lookupM i m ≡ just x → just m ≡ e
      new : lookupM i m ≡ nothing → just (insert i x m) ≡ e
-     wrong : (x' : A) → ¬(x ≡ x') → lookupM i m ≡ just x' → nothing ≡ e
+     wrong : (x' : A) → x ≢ x' → lookupM i m ≡ just x' → nothing ≡ e
 
 lift-checkInsertProof : {A : Set} {n : ℕ} {eq : EqInst A} {i : Fin n} {x : A} {m : FinMapMaybe n A} {e : Maybe (FinMapMaybe n A)} → checkInsertEqualProof eq i x m e → checkInsertProof eq i x m (checkInsert eq i x m ≡ e)
 lift-checkInsertProof {_} {_} {eq} {i} {x} {m} o = record
diff --git a/FinMap.agda b/FinMap.agda
index fce6384..4fc3e18 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -9,9 +9,9 @@ open import Data.Vec.Properties using (lookup∘tabulate)
 open import Data.List using (List ; [] ; _∷_ ; map ; zip)
 open import Data.Product using (_×_ ; _,_)
 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 ; contraposition)
-open import Relation.Binary.Core using (_≡_ ; refl)
+open import Relation.Binary.Core using (_≡_ ; refl ; _≢_)
 open import Relation.Binary.PropositionalEquality using (cong ; sym ; _≗_ ; trans)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 
@@ -62,7 +62,7 @@ lemma-lookupM-insert : {A : Set} {n : ℕ} → (i : Fin n) → (a : A) → (m :
 lemma-lookupM-insert zero    _ (_ ∷ _)  = refl
 lemma-lookupM-insert (suc i) a (_ ∷ xs) = lemma-lookupM-insert i a xs
 
-lemma-lookupM-insert-other : {A : Set} {n : ℕ} → (i j : Fin n) → (a : A) → (m : FinMapMaybe n A) → ¬(i ≡ j) → lookupM i m ≡ lookupM i (insert j a m)
+lemma-lookupM-insert-other : {A : Set} {n : ℕ} → (i j : Fin n) → (a : A) → (m : FinMapMaybe n A) → i ≢ j → lookupM i m ≡ lookupM i (insert j a m)
 lemma-lookupM-insert-other zero    zero    a m        p = contradiction refl p
 lemma-lookupM-insert-other zero    (suc j) a (x ∷ xs) p = refl
 lemma-lookupM-insert-other (suc i) zero    a (x ∷ xs) p = refl