diff options
Diffstat (limited to 'CheckInsert.agda')
| -rw-r--r-- | CheckInsert.agda | 8 |
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 |