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

Expose bundle form 'Map'

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-02-11 21:12:49 -08:00
parent bfb32092c2
commit e89418d600
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/Map.agda
View File

@ -882,6 +882,14 @@ isLattice = record
; absorb-⊓-⊔ = absorb-⊓-⊔ ; absorb-⊓-⊔ = absorb-⊓-⊔
} }
lattice : Lattice Map
lattice = record
{ _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isLattice = isLattice
}
⊔-equal-keys : ∀ {m₁ m₂ : Map} → keys m₁ ≡ keys m₂ → keys m₁ ≡ keys (m₁ ⊔ m₂) ⊔-equal-keys : ∀ {m₁ m₂ : Map} → keys m₁ ≡ keys m₂ → keys m₁ ≡ keys (m₁ ⊔ m₂)
⊔-equal-keys km₁≡km₂ = union-equal-keys km₁≡km₂ ⊔-equal-keys km₁≡km₂ = union-equal-keys km₁≡km₂