From a07a9d6ea38c55aeac59cb93678b9c830ce54705 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Tue, 7 Jul 2026 13:32:20 -0700 Subject: Update circuit values --- Lattice/Structure/IsBoundedDistributive.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Lattice/Structure') diff --git a/Lattice/Structure/IsBoundedDistributive.agda b/Lattice/Structure/IsBoundedDistributive.agda index dfd67d8..6128187 100644 --- a/Lattice/Structure/IsBoundedDistributive.agda +++ b/Lattice/Structure/IsBoundedDistributive.agda @@ -27,8 +27,6 @@ record IsBoundedDistributiveLattice minimum : Minimum _≤_ ⊥ ∧-distribˡ-∨ : _DistributesOverˡ_ _≈_ _∧_ _∨_ - open IsLattice isLattice public - isBoundedLattice : IsBoundedLattice _∨_ _∧_ ⊤ ⊥ isBoundedLattice = record { isLattice = isLattice @@ -41,3 +39,5 @@ record IsBoundedDistributiveLattice { isLattice = isLattice ; ∧-distribˡ-∨ = ∧-distribˡ-∨ } + + open IsBoundedLattice isBoundedLattice public -- cgit v1.2.3