From 6384f7006e3865bd9a52a83519094d9b61451166 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 18 Feb 2024 20:18:38 -0800
Subject: [PATCH] Make 'lattice' public

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice/IterProd.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Lattice/IterProd.agda b/Lattice/IterProd.agda
index 6e03454..00cbe43 100644
--- a/Lattice/IterProd.agda
+++ b/Lattice/IterProd.agda
@@ -20,7 +20,7 @@ IterProd k = iterate k (λ t → A × t) B
 -- To make iteration more convenient, package the definitions in Lattice
 -- records, perform the recursion, and unpackage.
 
-private module _ where
+module _ where
     lattice : ∀ {k : ℕ} → Lattice (IterProd k)
     lattice {0} = record
         { _≈_ = _≈₂_