Remove some unused imports (#732)

* remove some unused imports in RingSolver * remove some more unused imports (found with agda-unused) Co-authored-by: Matthias Hutzler <[email protected]>
agda · Mar 10, 2022 · 7d0daf3 · 7d0daf3
1 parent 6317041
commit 7d0daf3
Show file tree

Hide file tree

Showing 7 changed files with 0 additions and 11 deletions.
diff --git a/Cubical/Algebra/RingSolver/RawAlgebra.agda b/Cubical/Algebra/RingSolver/RawAlgebra.agda
@@ -2,7 +2,6 @@
 module Cubical.Algebra.RingSolver.RawAlgebra where
 
 open import Cubical.Foundations.Prelude
-open import Cubical.Data.Sigma
 open import Cubical.Data.Nat using (ℕ)
 open import Cubical.Data.Int renaming (_+_ to _+ℤ_ ; _·_ to _·ℤ_ ; -_ to -ℤ_ ; _-_ to _-ℤ_ ; +Assoc to +ℤAssoc ; +Comm to +ℤComm ; -DistL· to -ℤDistL·ℤ)
 

diff --git a/Cubical/Algebra/RingSolver/RawRing.agda b/Cubical/Algebra/RingSolver/RawRing.agda
@@ -2,8 +2,6 @@
 module Cubical.Algebra.RingSolver.RawRing where
 
 open import Cubical.Foundations.Prelude
-open import Cubical.Data.Sigma
-open import Cubical.Data.Nat using (ℕ)
 
 private
   variable

diff --git a/Cubical/Data/Bool/Base.agda b/Cubical/Data/Bool/Base.agda
@@ -1,16 +1,13 @@
 {-# OPTIONS --safe #-}
 module Cubical.Data.Bool.Base where
 
-open import Cubical.Core.Everything
-
 open import Cubical.Foundations.Prelude
 
 open import Cubical.Data.Empty
 open import Cubical.Data.Sum.Base
 open import Cubical.Data.Unit.Base
 
 open import Cubical.Relation.Nullary.Base
-open import Cubical.Relation.Nullary.DecidableEq
 
 -- Obtain the booleans
 open import Agda.Builtin.Bool public

diff --git a/Cubical/Data/Empty/Base.agda b/Cubical/Data/Empty/Base.agda
@@ -1,7 +1,6 @@
 {-# OPTIONS --safe #-}
 module Cubical.Data.Empty.Base where
 
-open import Cubical.Core.Everything
 open import Cubical.Foundations.Prelude
 
 private

diff --git a/Cubical/Foundations/Equiv.agda b/Cubical/Foundations/Equiv.agda
@@ -20,7 +20,6 @@ module Cubical.Foundations.Equiv where
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Isomorphism
-open import Cubical.Foundations.GroupoidLaws
 
 open import Cubical.Foundations.Equiv.Base public
 open import Cubical.Data.Sigma.Base

diff --git a/Cubical/Foundations/Isomorphism.agda b/Cubical/Foundations/Isomorphism.agda
@@ -16,8 +16,6 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Equiv.Base
 
-open import Cubical.Foundations.Function
-
 private
   variable
     ℓ ℓ' : Level

diff --git a/Cubical/Functions/Morphism.agda b/Cubical/Functions/Morphism.agda
@@ -6,7 +6,6 @@ module Cubical.Functions.Morphism where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Isomorphism
-open import Cubical.Foundations.Function
 
 open Iso
 module ax {ℓ : Level} (A : Type ℓ) (_+A_ : A → A → A) (a₀ : A) where