mirror of
https://github.com/Smaug123/agdaproofs
synced 2025-10-09 05:48:41 +00:00
21 lines
1018 B
Agda
21 lines
1018 B
Agda
{-# OPTIONS --warning=error --safe --without-K #-}
|
||
|
||
open import LogicalFormulae
|
||
open import Maybe
|
||
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
|
||
|
||
open import Numbers.Naturals.Semiring
|
||
|
||
module KeyValue.KeyValue {a b : _} (keys : Set a) (values : Set b) where
|
||
|
||
record KeyValue {c : _} (maps : Set c) : Set (a ⊔ b ⊔ c) where
|
||
field
|
||
tryFind : maps → keys → Maybe values
|
||
add : (map : maps) → keys → values → maps
|
||
empty : maps
|
||
count : maps → ℕ
|
||
lookupAfterAdd : (map : maps) → (k : keys) → (v : values) → tryFind (add map k v) k ≡ yes v
|
||
lookupAfterAdd' : (map : maps) → (k1 : keys) → (v : values) → (k2 : keys) → (k1 ≡ k2) || (tryFind (add map k1 v) k2 ≡ tryFind map k2)
|
||
countAfterAdd' : (map : maps) → (k : keys) → (v : values) → (tryFind map k ≡ no) → count (add map k v) ≡ succ (count map)
|
||
countAfterAdd : (map : maps) → (k : keys) → (v1 v2 : values) → (tryFind map k ≡ yes v2) → count (add map k v1) ≡ count map
|