From 6e26aa15808353d31fdc3bc5e75415c7ab2d820f Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 11 Feb 2024 21:02:43 -0800
Subject: [PATCH] Add a bundle to FiniteMap

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice/FiniteMap.agda | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/Lattice/FiniteMap.agda b/Lattice/FiniteMap.agda
index c2342a9..0a82eeb 100644
--- 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
+        }