DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Expose more functions from FiniteMap

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-05-08 20:50:05 -07:00
parent 6b116ed960
commit cfa3375de5
1 changed files with 8 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
Lattice/FiniteMap.agda
View File

@ -38,6 +38,8 @@ open import Lattice.Map ≡-dec-A lB as Map
; updating-via-k∈ks to updatingᵐ-via-k∈ks
; updating-via-k∈ks-≡ to updatingᵐ-via-k∈ks-≡
; updating-via-∈k-forward to updatingᵐ-via-∈k-forward
; updating-via-k∉ks-forward to updatingᵐ-via-k∉ks-forward
; updating-via-k∉ks-backward to updatingᵐ-via-k∉ks-backward
; f'-Monotonic to f'-Monotonicᵐ
; _≼_ to _≼ᵐ_
; ∈k-dec to ∈k-decᵐ
@ -185,6 +187,12 @@ module WithKeys (ks : List A) where
f'-k∈ks-≡ : ∀ {k v l} → k ∈ˡ ks → (k , v) ∈ (f' l) → v ≡ updater l k
f'-k∈ks-≡ {k} {v} {l} = updatingᵐ-via-k∈ks-≡ (proj₁ (f l)) (updater l)
f'-k∉ks-forward : ∀ {k v l} → ¬ k ∈ˡ ks → (k , v) ∈ (f l) → (k , v) ∈ (f' l)
f'-k∉ks-forward {k} {v} {l} = updatingᵐ-via-k∉ks-forward (proj₁ (f l)) (updater l)
f'-k∉ks-backward : ∀ {k v l} → ¬ k ∈ˡ ks → (k , v) ∈ (f' l) → (k , v) ∈ (f l)
f'-k∉ks-backward {k} {v} {l} = updatingᵐ-via-k∉ks-backward (proj₁ (f l)) (updater l)
all-equal-keys : ∀ (fm₁ fm₂ : FiniteMap) → (Map.keys (proj₁ fm₁) ≡ Map.keys (proj₁ fm₂))
all-equal-keys (fm₁ , km₁≡ks) (fm₂ , km₂≡ks) = trans km₁≡ks (sym km₂≡ks)