From cfa3375de5be97fd93bd83fe83a101abe540cd17 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Wed, 8 May 2024 20:50:05 -0700 Subject: [PATCH] Expose more functions from FiniteMap Signed-off-by: Danila Fedorin --- Lattice/FiniteMap.agda | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Lattice/FiniteMap.agda b/Lattice/FiniteMap.agda index 76f9722..aa45fc1 100644 --- a/Lattice/FiniteMap.agda +++ b/Lattice/FiniteMap.agda @@ -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)