Expose more functionaity from the set lattice
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
0c088ca2ae
commit
702cf2c298
|
@ -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
|
||||
|
|
Loading…
Reference in New Issue
Block a user