rewrite checkInsert using "... |" notation

Less characters => more readable.

1 files changed, 4 insertions, 4 deletions

diff --git a/CheckInsert.agda b/CheckInsert.agda
index 6b5473a..600b754 100644
--- a/CheckInsert.agda
+++ b/CheckInsert.agda
@@ -17,10 +17,10 @@ open import FinMap
 
 checkInsert : {n : ℕ} → Fin n → Carrier → FinMapMaybe n Carrier → Maybe (FinMapMaybe n Carrier)
 checkInsert i b m with lookupM i m
-checkInsert i b m | just c with deq b c
-checkInsert i b m | just .b | yes refl = just m
-checkInsert i b m | just c  | no ¬p    = nothing
-checkInsert i b m | nothing = just (insert i b m)
+...               | nothing = just (insert i b m)
+...               | just c with deq b c
+...                         | yes b≡c = just m
+...                         | no b≢c  = nothing
 
 record checkInsertProof {n : ℕ} (i : Fin n) (x : Carrier) (m : FinMapMaybe n Carrier) (P : Set) : Set where
   field