From 29898e738b5994f68a045d51a54e7db67d9dac98 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 1 Mar 2024 19:08:29 -0800 Subject: [PATCH] Clean up a bit Signed-off-by: Danila Fedorin --- Lattice/FiniteValueMap.agda | 2 -- 1 file changed, 2 deletions(-) diff --git a/Lattice/FiniteValueMap.agda b/Lattice/FiniteValueMap.agda index 3fc0cd9..30783b5 100644 --- a/Lattice/FiniteValueMap.agda +++ b/Lattice/FiniteValueMap.agda @@ -224,8 +224,6 @@ module IterProdIsomorphism where ) - -- Provenance-union : ∀ {ks : List A} (fm₁ fm₂ : FiniteMap ks) (k : A) (v : B) → (k , v) ∈ᵐ (fm₁ ⊔ᵐ fm₂) → Σ (B × B) (λ (v₁ , v₂) → ((v ≡ v₁ ⊔₂ v₂) × ((k , v₁) ∈ᵐ fm₁ × (k , v₂) ∈ᵐ fm₂))) - to-⊔-distr : ∀ {ks : List A} (uks : Unique ks) → (ip₁ ip₂ : IterProd (length ks)) → to uks (_⊔ⁱᵖ_ {ks} ip₁ ip₂) ≈ᵐ (to uks ip₁ ⊔ᵐ to uks ip₂) to-⊔-distr {[]} empty tt tt = ((λ k v ()), (λ k v ())) to-⊔-distr {ks@(k ∷ ks')} uks@(push k≢ks' uks') ip₁@(v₁ , rest₁) ip₂@(v₂ , rest₂) = (fm⊆fm₁fm₂ , fm₁fm₂⊆fm)