From b1ff726734b60d82270fb77a0bdc70ecea20a9b5 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Fri, 2 Nov 2012 15:19:40 +0100
Subject: rewrite checkInsert using "... |" notation

Less characters => more readable.
---
 CheckInsert.agda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'CheckInsert.agda')

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
-- 
cgit v1.2.3