From 3305de47101b596126d96579575fea55ec4c42a5 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 10 Mar 2024 18:35:29 -0700
Subject: [PATCH] Remove need for explicit arguments in map derivatives

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Language.agda                       |  2 +-
 Lattice/Bundles/FiniteValueMap.agda |  4 ++--
 Lattice/FiniteMap.agda              |  8 ++++----
 Lattice/FiniteValueMap.agda         | 10 +++++-----
 Lattice/Map.agda                    |  6 +++---
 Lattice/MapSet.agda                 |  4 ++--
 6 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/Language.agda b/Language.agda
index 50c2ae9..4bf0be7 100644
--- a/Language.agda
+++ b/Language.agda
@@ -26,7 +26,7 @@ data Expr : Set where
 data Stmt : Set where
     _←_ : String → Expr → Stmt
 
-open import Lattice.MapSet String _≟ˢ_
+open import Lattice.MapSet _≟ˢ_
     renaming
         ( MapSet to StringSet
         ; insert to insertˢ
diff --git a/Lattice/Bundles/FiniteValueMap.agda b/Lattice/Bundles/FiniteValueMap.agda
index 26506de..41ecf30 100644
--- a/Lattice/Bundles/FiniteValueMap.agda
+++ b/Lattice/Bundles/FiniteValueMap.agda
@@ -20,11 +20,11 @@ module FromFiniteHeightLattice (fhB : FiniteHeightLattice B)
         )
 
     import Lattice.FiniteMap
-    module FM = Lattice.FiniteMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A isLattice₂
+    module FM = Lattice.FiniteMap ≡-dec-A isLattice₂
     open FM.WithKeys ks public
 
     import Lattice.FiniteValueMap
-    module FVM = Lattice.FiniteValueMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A isLattice₂
+    module FVM = Lattice.FiniteValueMap ≡-dec-A isLattice₂
     open FVM.IterProdIsomorphism.WithUniqueKeysAndFixedHeight uks ≈₂-dec height₂ fixedHeight₂ public
 
     ≈-dec = ≈₂-dec⇒≈-dec ≈₂-dec
diff --git a/Lattice/FiniteMap.agda b/Lattice/FiniteMap.agda
index 48f7b00..87c3d78 100644
--- a/Lattice/FiniteMap.agda
+++ b/Lattice/FiniteMap.agda
@@ -4,14 +4,14 @@ open import Relation.Binary.PropositionalEquality as Eq
 open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
 open import Data.List using (List; _∷_; [])
 
-module Lattice.FiniteMap {a b : Level} (A : Set a) (B : Set b)
-    (_≈₂_ : B → B → Set b)
-    (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
+module Lattice.FiniteMap {a b : Level} {A : Set a} {B : Set b}
+    {_≈₂_ : B → B → Set b}
+    {_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B}
     (≡-dec-A : IsDecidable (_≡_ {a} {A}))
     (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
 
 open IsLattice lB using () renaming (_≼_ to _≼₂_)
-open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB as Map
+open import Lattice.Map ≡-dec-A lB as Map
     using (Map; ⊔-equal-keys; ⊓-equal-keys; ∈k-dec; m₁≼m₂⇒m₁[k]≼m₂[k])
     renaming
         ( _≈_ to _≈ᵐ_
diff --git a/Lattice/FiniteValueMap.agda b/Lattice/FiniteValueMap.agda
index d5e4bce..c4c3c3c 100644
--- a/Lattice/FiniteValueMap.agda
+++ b/Lattice/FiniteValueMap.agda
@@ -10,9 +10,9 @@ open import Relation.Binary.Definitions using (Decidable)
 open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
 open import Function.Definitions using (Inverseˡ; Inverseʳ)
 
-module Lattice.FiniteValueMap (A : Set) (B : Set)
-    (_≈₂_ : B → B → Set)
-    (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
+module Lattice.FiniteValueMap {A : Set} {B : Set}
+    {_≈₂_ : B → B → Set}
+    {_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B}
     (≡-dec-A : Decidable (_≡_ {_} {A}))
     (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
 
@@ -29,7 +29,7 @@ open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Relation.Nullary using (¬_)
 open import Isomorphism using (IsInverseˡ; IsInverseʳ)
 
-open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB
+open import Lattice.Map ≡-dec-A lB
     using
         ( subset-impl
         ; locate; forget
@@ -40,7 +40,7 @@ open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB
         ; in₁; in₂; bothᵘ; single
         ; ⊔-combines
         )
-open import Lattice.FiniteMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB public
+open import Lattice.FiniteMap ≡-dec-A lB public
 
 module IterProdIsomorphism where
     open import Data.Unit using (⊤; tt)
diff --git a/Lattice/Map.agda b/Lattice/Map.agda
index f2d1364..afc86cd 100644
--- a/Lattice/Map.agda
+++ b/Lattice/Map.agda
@@ -3,9 +3,9 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym;
 open import Relation.Binary.Definitions using (Decidable)
 open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
 
-module Lattice.Map {a b : Level} (A : Set a) (B : Set b)
-    (_≈₂_ : B → B → Set b)
-    (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
+module Lattice.Map {a b : Level} {A : Set a} {B : Set b}
+    {_≈₂_ : B → B → Set b}
+    {_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B}
     (≡-dec-A : Decidable (_≡_ {a} {A}))
     (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
 
diff --git a/Lattice/MapSet.agda b/Lattice/MapSet.agda
index 2ce73c3..61ca0d5 100644
--- a/Lattice/MapSet.agda
+++ b/Lattice/MapSet.agda
@@ -3,7 +3,7 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym;
 open import Relation.Binary.Definitions using (Decidable)
 open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
 
-module Lattice.MapSet {a : Level} (A : Set a) (≡-dec-A : Decidable (_≡_ {a} {A})) where
+module Lattice.MapSet {a : Level} {A : Set a} (≡-dec-A : Decidable (_≡_ {a} {A})) where
 
 open import Data.List using (List; map)
 open import Data.Product using (_,_; proj₁)
@@ -12,7 +12,7 @@ open import Function using (_∘_)
 open import Lattice.Unit using (⊤; tt) renaming (_≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_; isLattice to ⊤-isLattice)
 import Lattice.Map
 
-private module UnitMap = Lattice.Map A ⊤ _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A ⊤-isLattice
+private module UnitMap = Lattice.Map ≡-dec-A ⊤-isLattice
 open UnitMap
     using (Map; Expr; ⟦_⟧)
     renaming