drop the insert- prefix from the insertionresult ctors

2 files changed, 15 insertions, 15 deletions

diff --git a/Bidir.agda b/Bidir.agda
index ef3b397..4428bba 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -41,9 +41,9 @@ lemma-lookupM-assoc : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (
 lemma-lookupM-assoc i is x xs h    p with assoc is xs
 lemma-lookupM-assoc i is x xs h    () | nothing
 lemma-lookupM-assoc i is x xs h    p | just h' with checkInsert i x h' | insertionresult i x h'
-lemma-lookupM-assoc i is x xs .h refl | just h | ._ | insert-same pl = pl
-lemma-lookupM-assoc i is x xs ._ refl | just h' | ._ | insert-new _ = lemma-lookupM-insert i x h'
-lemma-lookupM-assoc i is x xs h () | just h' | ._ | insert-wrong _ _ _
+lemma-lookupM-assoc i is x xs .h refl | just h | ._ | same pl = pl
+lemma-lookupM-assoc i is x xs ._ refl | just h' | ._ | new _ = lemma-lookupM-insert i x h'
+lemma-lookupM-assoc i is x xs h () | just h' | ._ | wrong _ _ _
 
 lemma-∉-lookupM-assoc : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (xs : Vec Carrier m) → (h : FinMapMaybe n Carrier) → assoc is xs ≡ just h → (i ∉ toList is) → lookupM i h ≡ nothing
 lemma-∉-lookupM-assoc i []         []         .empty refl i∉is = lemma-lookupM-empty i
@@ -64,13 +64,13 @@ lemma-assoc-domain []         []         h ph = Data.List.All.[]
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') h ph with assoc is' xs' | inspect (assoc is') xs'
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') h () | nothing | [ ph' ]
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') h ph | just h' | [ ph' ] with checkInsert i' x' h' | inspect (checkInsert i' x') h' | insertionresult i' x' h'
-lemma-assoc-domain (i' ∷ is') (x' ∷ xs') .h refl | just h | [ ph' ] | ._ | _ | insert-same pl = All._∷_ (x' , pl) (lemma-assoc-domain is' xs' h ph')
-lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ._ refl | just h' | [ ph' ] | ._ | [ cI≡ ] | insert-new _ = All._∷_
+lemma-assoc-domain (i' ∷ is') (x' ∷ xs') .h refl | just h | [ ph' ] | ._ | _ | same pl = All._∷_ (x' , pl) (lemma-assoc-domain is' xs' h ph')
+lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ._ refl | just h' | [ ph' ] | ._ | [ cI≡ ] | new _ = All._∷_
   (x' , lemma-lookupM-insert i' x' h')
   (Data.List.All.map
     (λ {i} p → proj₁ p , lemma-lookupM-checkInsert i i' (proj₁ p) x' h' (insert i' x' h') (proj₂ p) cI≡)
     (lemma-assoc-domain is' xs' h' ph'))
-lemma-assoc-domain (i' ∷ is') (x' ∷ xs') h () | just h' | [ ph' ] | ._ | _ | insert-wrong _ _ _
+lemma-assoc-domain (i' ∷ is') (x' ∷ xs') h () | just h' | [ ph' ] | ._ | _ | wrong _ _ _
 
 lemma-map-lookupM-insert : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (x : Carrier) → (h : FinMapMaybe n Carrier) → i ∉ (toList is) → map (flip lookupM (insert i x h)) is ≡ map (flip lookupM h) is
 lemma-map-lookupM-insert i []         x h i∉is = refl
diff --git a/CheckInsert.agda b/CheckInsert.agda
index 8c1aa20..142cc61 100644
--- a/CheckInsert.agda
+++ b/CheckInsert.agda
@@ -23,16 +23,16 @@ checkInsert i b m with lookupM i m
 ...                         | no b≢c  = nothing
 
 data InsertionResult {n : ℕ} (i : Fin n) (x : Carrier) (h : FinMapMaybe n Carrier) : Maybe (FinMapMaybe n Carrier) → Set where
-  insert-same : lookupM i h ≡ just x → InsertionResult i x h (just h)
-  insert-new : lookupM i h ≡ nothing → InsertionResult i x h (just (insert i x h))
-  insert-wrong : (x' : Carrier) → x ≢ x' → lookupM i h ≡ just x' → InsertionResult i x h nothing
+  same : lookupM i h ≡ just x → InsertionResult i x h (just h)
+  new : lookupM i h ≡ nothing → InsertionResult i x h (just (insert i x h))
+  wrong : (x' : Carrier) → x ≢ x' → lookupM i h ≡ just x' → InsertionResult i x h nothing
 
 insertionresult : {n : ℕ} → (i : Fin n) → (x : Carrier) → (h : FinMapMaybe n Carrier) → InsertionResult i x h (checkInsert i x h)
 insertionresult i x h with lookupM i h | inspect (lookupM i) h
 insertionresult i x h | just x' | _ with deq x x'
-insertionresult i x h | just .x | [ il ] | yes refl = insert-same il
-insertionresult i x h | just x' | [ il ] | no x≢x' = insert-wrong x' x≢x' il
-insertionresult i x h | nothing | [ il ] = insert-new il
+insertionresult i x h | just .x | [ il ] | yes refl = same il
+insertionresult i x h | just x' | [ il ] | no x≢x' = wrong x' x≢x' il
+insertionresult i x h | nothing | [ il ] = new il
 
 lemma-checkInsert-same : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → lookupM i m ≡ just x → checkInsert i x m ≡ just m
 lemma-checkInsert-same i x m p with lookupM i m
@@ -52,9 +52,9 @@ lemma-checkInsert-wrong i x m x' d refl | .(just x') | no ¬q = refl
 
 lemma-checkInsert-restrict : {n : ℕ} → (f : Fin n → Carrier) → (i : Fin n) → (is : List (Fin n)) → checkInsert i (f i) (restrict f is) ≡ just (restrict f (i ∷ is))
 lemma-checkInsert-restrict f i is with checkInsert i (f i) (restrict f is) | insertionresult i (f i) (restrict f is)
-lemma-checkInsert-restrict f i is | ._ | insert-same p = cong just (lemma-insert-same _ i (f i) p)
-lemma-checkInsert-restrict f i is | ._ | insert-new _ = refl
-lemma-checkInsert-restrict f i is | ._ | insert-wrong x fi≢x p = contradiction (lemma-lookupM-restrict i f is x p) fi≢x
+lemma-checkInsert-restrict f i is | ._ | same p = cong just (lemma-insert-same _ i (f i) p)
+lemma-checkInsert-restrict f i is | ._ | new _ = refl
+lemma-checkInsert-restrict f i is | ._ | wrong x fi≢x p = contradiction (lemma-lookupM-restrict i f is x p) fi≢x
 
 lemma-lookupM-checkInsert : {n : ℕ} → (i j : Fin n) → (x y : Carrier) → (h h' : FinMapMaybe n Carrier) → lookupM i h ≡ just x → checkInsert j y h ≡ just h' → lookupM i h' ≡ just x
 lemma-lookupM-checkInsert i j x y h h' pl ph' with lookupM j h | inspect (lookupM j) h