From 70847d51db6858eb8a2b85a466e3be32b27bd5b6 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 4 Jan 2025 21:23:07 -0800
Subject: [PATCH] Swich AboveBelow to using instances

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Analysis/Sign.agda      | 15 ++++++++++++---
 Lattice/AboveBelow.agda |  7 ++++---
 2 files changed, 16 insertions(+), 6 deletions(-)

diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda
index 913a341..4d0721c 100644
--- a/Analysis/Sign.agda
+++ b/Analysis/Sign.agda
@@ -13,6 +13,7 @@ open import Relation.Nullary using (¬_; yes; no)
 
 open import Language
 open import Lattice
+open import Equivalence
 open import Showable using (Showable; show)
 open import Utils using (_⇒_; _∧_; _∨_)
 import Analysis.Forward
@@ -44,11 +45,19 @@ _≟ᵍ_ 0ˢ + = no (λ ())
 _≟ᵍ_ 0ˢ - = no (λ ())
 _≟ᵍ_ 0ˢ 0ˢ = yes refl
 
-≡-Decidable-Sign : IsDecidable {_} {Sign} _≡_
-≡-Decidable-Sign = record { R-dec = _≟ᵍ_ }
+instance
+    ≡-equiv : IsEquivalence Sign _≡_
+    ≡-equiv = record
+        { ≈-refl = refl
+        ; ≈-sym = sym
+        ; ≈-trans = trans
+        }
+
+    ≡-Decidable-Sign : IsDecidable {_} {Sign} _≡_
+    ≡-Decidable-Sign = record { R-dec = _≟ᵍ_ }
 
 -- embelish 'sign' with a top and bottom element.
-open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) ≡-Decidable-Sign as AB
+open import Lattice.AboveBelow Sign _ as AB
     using ()
     renaming
         ( AboveBelow to SignLattice
diff --git a/Lattice/AboveBelow.agda b/Lattice/AboveBelow.agda
index 2cce13f..5532e7e 100644
--- a/Lattice/AboveBelow.agda
+++ b/Lattice/AboveBelow.agda
@@ -1,11 +1,12 @@
 open import Lattice
 open import Equivalence
 open import Relation.Nullary using (Dec; ¬_; yes; no)
+open import Data.Unit using () renaming (⊤ to ⊤ᵘ)
 
 module Lattice.AboveBelow {a} (A : Set a)
-                          (_≈₁_ : A → A → Set a)
-                          (≈₁-equiv : IsEquivalence A _≈₁_)
-                          (≈₁-Decidable : IsDecidable _≈₁_) where
+                          {_≈₁_ : A → A → Set a}
+                          {{≈₁-equiv : IsEquivalence A _≈₁_}}
+                          {{≈₁-Decidable : IsDecidable _≈₁_}} (dummy : ⊤ᵘ) where
 
 open import Data.Empty using (⊥-elim)
 open import Data.Product using (_,_)