Add a bundle to FiniteMap

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 21:02:43 -08:00 · 2024-02-11 21:02:43 -08:00 · 6e26aa1580
commit 6e26aa1580
parent 27f40bd42e
1 changed files with 8 additions and 0 deletions
--- a/Lattice/FiniteMap.agda
+++ b/Lattice/FiniteMap.agda
@ -76,3 +76,11 @@ module _ (ks : List A) where
        ; absorb-⊔-⊓ = λ (m₁ , _) (m₂ , _) → absorb-⊔ᵐ-⊓ᵐ m₁ m₂
        ; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) → absorb-⊓ᵐ-⊔ᵐ m₁ m₂
        }
+
+    lattice : Lattice FiniteMap
+    lattice = record
+        { _≈_ = _≈_
+        ; _⊔_ = _⊔_
+        ; _⊓_ = _⊓_
+        ; isLattice = isLattice
+        }