From 702cf2c29892d0cc3e4212749188e70825c84397 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 9 Mar 2024 13:58:40 -0800 Subject: [PATCH] Expose more functionaity from the set lattice Signed-off-by: Danila Fedorin --- Lattice/MapSet.agda | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/Lattice/MapSet.agda b/Lattice/MapSet.agda index c41de8c..17285da 100644 --- a/Lattice/MapSet.agda +++ b/Lattice/MapSet.agda @@ -5,15 +5,25 @@ open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_) module Lattice.MapSet {a : Level} (A : Set a) (≡-dec-A : Decidable (_≡_ {a} {A})) where -open import Lattice.Unit using (⊤) renaming (_≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_; isLattice to ⊤-isLattice) +open import Data.List using (List; map) +open import Data.Product using (proj₁) +open import Function using (_∘_) + +open import Lattice.Unit using (⊤; tt) renaming (_≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_; isLattice to ⊤-isLattice) import Lattice.Map private module UnitMap = Lattice.Map A ⊤ _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A ⊤-isLattice open UnitMap using (Map) open UnitMap using - ( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_ + ( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_; empty ; isUnionSemilattice; isIntersectSemilattice; isLattice; lattice ) public MapSet : Set a MapSet = Map + +to-List : MapSet → List A +to-List = map proj₁ ∘ proj₁ + +insert : A → MapSet → MapSet +insert k = UnitMap.insert k tt