style: sort some of the imports

RedPRL · Nov 27, 2023 · 0e8190e · 0e8190e
1 parent 147c8d9
commit 0e8190e
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 7 deletions.
diff --git a/src/Mugen/Algebra/Displacement/NearlyConstant.agda b/src/Mugen/Algebra/Displacement/NearlyConstant.agda
@@ -7,13 +7,12 @@ open import Algebra.Monoid
 open import Algebra.Semigroup
 
 open import Mugen.Prelude
+open import Mugen.Data.List
 open import Mugen.Order.Poset
 open import Mugen.Algebra.Displacement
 open import Mugen.Algebra.Displacement.InfiniteProduct
 open import Mugen.Algebra.OrderedMonoid
 
-open import Mugen.Data.List
-
 --------------------------------------------------------------------------------
 -- Nearly Constant Functions
 -- Section 3.3.5

diff --git a/src/Mugen/Order/Discrete.agda b/src/Mugen/Order/Discrete.agda
@@ -1,7 +1,5 @@
 module Mugen.Order.Discrete where
 
-open import Data.Fin
-
 open import Mugen.Prelude
 
 open import Mugen.Order.Poset

diff --git a/src/Mugen/Order/Poset.agda b/src/Mugen/Order/Poset.agda
@@ -1,7 +1,7 @@
-import Order.Base
-
 open import Mugen.Prelude
 
+import Order.Base
+
 module Mugen.Order.Poset where
 
 

diff --git a/src/Mugen/Order/Reasoning.agda b/src/Mugen/Order/Reasoning.agda
@@ -1,5 +1,5 @@
-open import Mugen.Prelude
 open import Mugen.Order.Poset
+open import Mugen.Prelude
 
 module Mugen.Order.Reasoning {o r} (A : Poset o r) where