[Import] Data.* (agda#2621)

* Import cleaning Data 2

* fix

---------

Co-authored-by: Jacques Carette <[email protected]>

Author: jmougeot

src/Data/Bool/Properties.agda

@@ -8,34 +8,41 @@
 
 module Data.Bool.Properties where
 open import Algebra.Bundles
-open import Algebra.Lattice.Bundles using
-  (BooleanAlgebra; DistributiveLattice; Lattice; Semilattice)
+  using (Magma; Semigroup; Band; CommutativeMonoid
+        ; IdempotentCommutativeMonoid; CommutativeSemiring; CommutativeRing)
+open import Algebra.Lattice.Bundles
+  using (Lattice; DistributiveLattice; BooleanAlgebra; Semilattice)
 import Algebra.Lattice.Properties.BooleanAlgebra as BooleanAlgebraProperties
-open import Data.Bool.Base using (Bool; T; _<_; _≤_; _∧_; _∨_; _xor_; b≤b; f<t;
-  f≤t; false; if_then_else_; not; true)
+open import Data.Bool.Base
+  using (Bool; true; false; not; _∧_; _∨_; _xor_ ; if_then_else_; T; _≤_; _<_
+        ; b≤b; f≤t; f<t)
 open import Data.Empty using (⊥; ⊥-elim)
-open import Data.Product.Base using (_,_; _×_; proj₁; proj₂)
-open import Data.Sum.Base using ([_,_]; _⊎_; inj₁; inj₂)
+open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
 open import Function.Base using (_⟨_⟩_; const; id)
 open import Function.Bundles hiding (Inverse; LeftInverse; RightInverse)
 open import Induction.WellFounded using (Acc; WellFounded; acc)
 open import Level using (0ℓ; Level)
 open import Relation.Binary.Bundles using (DecSetoid; DecTotalOrder; Poset;
   Preorder; Setoid; StrictPartialOrder; StrictTotalOrder; TotalOrder)
 open import Relation.Binary.Core using (_⇒_)
-open import Relation.Binary.Definitions using (Antisymmetric; Asymmetric;
-  Decidable; DecidableEquality; Irreflexive; Irrelevant; Maximum; Minimum;
-  Reflexive; Total; Trans; Transitive; Trichotomous; _Respects₂_;
-  tri<; tri>; tri≈)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_;
-  cong; cong₂; refl; subst; sym; trans)
-open import Relation.Binary.PropositionalEquality.Properties using
-  (decSetoid; isEquivalence; module ≡-Reasoning; setoid)
-open import Relation.Binary.Structures using (IsDecTotalOrder;
-  IsPartialOrder; IsPreorder; IsStrictPartialOrder; IsStrictTotalOrder;
-  IsTotalOrder)
-open import Relation.Nullary.Decidable.Core using (True; fromWitness; no; yes)
-import Relation.Unary as U using (Irrelevant)
+open import Relation.Binary.Structures
+  using (IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder
+        ; IsStrictPartialOrder; IsStrictTotalOrder)
+open import Relation.Binary.Bundles
+  using (Setoid; DecSetoid; Poset; Preorder; TotalOrder; DecTotalOrder
+        ; StrictPartialOrder; StrictTotalOrder)
+open import Relation.Binary.Definitions
+  using (Decidable; DecidableEquality ; Reflexive; Transitive; Antisymmetric
+        ; Minimum; Maximum; Total; Irrelevant ; Irreflexive; Asymmetric; Trans
+        ; Trichotomous; tri≈; tri<; tri>; _Respects₂_)
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_; refl; sym; cong; cong₂; subst; trans; _≢_)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning; setoid; decSetoid; isEquivalence)
+open import Relation.Nullary.Decidable.Core
+  using (True; yes; no; fromWitness ; toWitness)
+import Relation.Unary as U
 
 open import Algebra.Definitions {A = Bool} _≡_
 open import Algebra.Structures {A = Bool} _≡_

src/Data/Bool/Solver.agda

@@ -13,6 +13,7 @@ module Data.Bool.Solver where
 import Algebra.Solver.Ring.Simple as Solver
 import Algebra.Solver.Ring.AlmostCommutativeRing as ACR
 open import Data.Bool.Properties
+  using (_≟_;  ∨-∧-commutativeSemiring; xor-∧-commutativeRing)
 
 ------------------------------------------------------------------------
 -- A module for automatically solving propositional equivalences

src/Data/Bytestring/Base.agda

@@ -9,13 +9,12 @@
 
 module Data.Bytestring.Base where
 
-open import Data.Nat.Base using (ℕ; _+_; _*_; _^_)
 open import Agda.Builtin.String using (String)
+open import Data.Nat.Base using (ℕ; _+_; _*_; _^_)
 import Data.Fin.Base as Fin
 open import Data.Vec.Base as Vec using (Vec)
 open import Data.Word8.Base as Word8 using (Word8)
 open import Data.Word64.Base as Word64 using (Word64)
-
 open import Function.Base using (const; _$_)
 
 ------------------------------------------------------------------------------

src/Data/Bytestring/Builder/Primitive.agda

@@ -8,11 +8,9 @@
 
 module Data.Bytestring.Builder.Primitive where
 
-open import Agda.Builtin.Nat
-open import Agda.Builtin.String
-
-open import Data.Word8.Primitive
+open import Agda.Builtin.String using (String)
 open import Data.Bytestring.Primitive using (Bytestring)
+open import Data.Word8.Primitive using (Word8)
 
 infixr 6 _<>_
 

src/Data/Bytestring/IO.agda

@@ -8,7 +8,7 @@
 
 module Data.Bytestring.IO where
 
-open import Agda.Builtin.String
+open import Agda.Builtin.String using (String)
 open import IO using (IO; lift)
 open import Data.Bytestring.Base using (Bytestring)
 open import Data.Unit.Base using (⊤)

src/Data/Bytestring/IO/Primitive.agda

@@ -10,10 +10,9 @@ module Data.Bytestring.IO.Primitive where
 
 open import Agda.Builtin.String using (String)
 open import Agda.Builtin.Unit using (⊤)
+open import Data.Bytestring.Primitive using (Bytestring)
 open import IO.Primitive.Core using (IO)
 
-open import Data.Bytestring.Primitive
-
 postulate
   readFile : String → IO Bytestring
   writeFile : String → Bytestring → IO ⊤

src/Data/Char/Base.agda

@@ -8,13 +8,13 @@
 
 module Data.Char.Base where
 
-open import Level using (zero)
-import Data.Nat.Base as ℕ
+import Data.Nat.Base as ℕ using (_<_; _≡ᵇ_)
 open import Data.Bool.Base using (Bool)
 open import Function.Base using (_on_)
+open import Level using (zero)
 open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.PropositionalEquality.Core
-open import Relation.Binary.Construct.Closure.Reflexive
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_)
+open import Relation.Binary.Construct.Closure.Reflexive using (ReflClosure)
 
 ------------------------------------------------------------------------
 -- Re-export the type, and renamed primitives

src/Data/Char/Instances.agda

@@ -8,7 +8,7 @@
 
 module Data.Char.Instances where
 
-open import Data.Char.Properties
+open import Data.Char.Properties using (isDecEquivalence)
 
 instance
   Char-≡-isDecEquivalence = isDecEquivalence

src/Data/Char/Properties.agda

@@ -9,28 +9,38 @@
 module Data.Char.Properties where
 
 open import Data.Bool.Base using (Bool)
-open import Data.Char.Base
-import Data.Nat.Base as ℕ
+open import Data.Char.Base using (Char; _≈_; _≉_; _<_; _≤_; toℕ)
+import Data.Nat.Base as ℕ using (ℕ; _<_; _≤_)
 import Data.Nat.Properties as ℕ
+  using (_<?_; <-cmp; <-isStrictPartialOrder; <-isStrictTotalOrder
+        ; <-strictPartialOrder; <-strictTotalOrder; <-irrefl; <-trans; <-asym
+        ; _≟_)
 open import Data.Product.Base using (_,_)
-
-open import Function.Base
+open import Function.Base using (const; _∘′_)
 open import Relation.Nullary using (¬_; yes; no)
 open import Relation.Nullary.Decidable using (map′; isYes)
 open import Relation.Binary.Core using (_⇒_)
 open import Relation.Binary.Bundles
-  using (Setoid; DecSetoid; StrictPartialOrder; StrictTotalOrder; Preorder; Poset; DecPoset)
+  using (Setoid; DecSetoid; StrictPartialOrder; StrictTotalOrder; Preorder
+        ; Poset; DecPoset)
 open import Relation.Binary.Structures
-  using (IsDecEquivalence; IsStrictPartialOrder; IsStrictTotalOrder; IsPreorder; IsPartialOrder; IsDecPartialOrder; IsEquivalence)
+  using (IsDecEquivalence; IsStrictPartialOrder; IsStrictTotalOrder
+        ; IsPreorder; IsPartialOrder; IsDecPartialOrder; IsEquivalence)
 open import Relation.Binary.Definitions
-  using (Decidable; DecidableEquality; Trichotomous; Irreflexive; Transitive; Asymmetric; Antisymmetric; Symmetric; Substitutive; Reflexive; tri<; tri≈; tri>)
+  using (Decidable; DecidableEquality; Trichotomous; Irreflexive
+        ; Transitive; Asymmetric; Antisymmetric; Symmetric; Substitutive
+        ; Reflexive; tri<; tri≈; tri>)
 import Relation.Binary.Construct.On as On
-import Relation.Binary.Construct.Subst.Equality as Subst
+  using (decidable; transitive; asymmetric; isStrictPartialOrder
+        ; isStrictTotalOrder; strictPartialOrder; strictTotalOrder)
 import Relation.Binary.Construct.Closure.Reflexive as Refl
+  using (Refl; reflexive)
 import Relation.Binary.Construct.Closure.Reflexive.Properties as Refl
+  using (trans; antisym; decidable)
 open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; _≢_; refl; cong; sym; trans; subst)
-import Relation.Binary.PropositionalEquality.Properties as ≡
+import Relation.Binary.PropositionalEquality.Properties as ≡ using
+  (isDecEquivalence; setoid; decSetoid; isEquivalence)
 
 ------------------------------------------------------------------------
 -- Primitive properties
@@ -303,3 +313,4 @@ Please use <-strictPartialOrder instead."
 "Warning: <-strictTotalOrder-≈ was deprecated in v1.5.
 Please use <-strictTotalOrder instead."
 #-}
+

src/Data/Container/Indexed/Core.agda

@@ -8,9 +8,9 @@
 
 module Data.Container.Indexed.Core where
 
-open import Level
+open import Level using (Level; _⊔_; suc)
 open import Data.Product.Base using (Σ; Σ-syntax; _,_; ∃)
-open import Relation.Unary
+open import Relation.Unary using (Pred)
 
 private variable
   i o c r ℓ ℓ′ : Level

src/Data/Container/Indexed/FreeMonad.agda

@@ -8,17 +8,17 @@
 
 module Data.Container.Indexed.FreeMonad where
 
-open import Level
+open import Level using (Level; _⊔_; lower)
 open import Function.Base hiding (const)
-open import Effect.Monad.Predicate
-open import Data.Container.Indexed
+open import Effect.Monad.Predicate using (RawPMonad)
+open import Data.Container.Indexed using (Container; Command; Response; next; ⟦_⟧; μ)
 open import Data.Container.Indexed.Combinator hiding (id; _∘_)
-open import Data.Empty
+open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Product.Base using (_,_)
-open import Data.W.Indexed
-open import Relation.Unary
-open import Relation.Unary.PredicateTransformer
+open import Data.W.Indexed using (sup)
+open import Relation.Unary using (Pred; _⊆_; ⋃; _∈_; ｛_｝)
+open import Relation.Unary.PredicateTransformer using (Pt)
 open import Relation.Binary.PropositionalEquality.Core using (refl)
 
 ------------------------------------------------------------------------

src/Data/Container/Indexed/Relation/Binary/Equality/Setoid.agda

@@ -14,10 +14,10 @@ module Data.Container.Indexed.Relation.Binary.Equality.Setoid
 
 open import Function
 open import Level using (Level; _⊔_; suc)
-open import Relation.Binary
-
-open import Data.Container.Indexed.Core
-open import Data.Container.Indexed.Relation.Binary.Pointwise
+open import Relation.Binary using (Reflexive; Symmetric; Transitive; IsEquivalence)
+open import Relation.Binary.Core using (Rel)
+open import Data.Container.Indexed.Core using (Container; ⟦_⟧)
+open import Data.Container.Indexed.Relation.Binary.Pointwise using (Pointwise)
 import Data.Container.Indexed.Relation.Binary.Pointwise.Properties
   as Pointwise
 

src/Data/Container/Indexed/Relation/Binary/Pointwise.agda

@@ -9,13 +9,12 @@
 module Data.Container.Indexed.Relation.Binary.Pointwise where
 
 open import Data.Product.Base using (_,_; Σ-syntax)
+open import Data.Container.Indexed.Core using (Container; Subtrees; ⟦_⟧)
 open import Function.Base using (_∘_)
 open import Level using (Level; _⊔_)
 open import Relation.Binary using (REL; _⇒_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
-open import Data.Container.Indexed.Core using (Container; Subtrees; ⟦_⟧)
-
 private variable
   ℓᵉ ℓᵉ′ ℓᵖ ℓˢ ℓˣ ℓʸ : Level
   I O : Set _

src/Data/Container/Indexed/WithK.agda

@@ -18,11 +18,12 @@ open import Data.Container.Indexed hiding (module PlainMorphism)
 open import Data.Product.Base
   using (_,_; -,_; _×_; ∃; proj₁; proj₂; Σ-syntax)
 open import Function.Base renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_)
-open import Level
+open import Level using (Level; _⊔_)
 open import Relation.Unary using (Pred; _⊆_)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl)
 open import Relation.Binary.HeterogeneousEquality as ≅ using (_≅_; refl)
 open import Relation.Binary.Indexed.Heterogeneous
+  using (IndexedSetoid; Transitive; Symmetric; IREL; IRel)
 
 ------------------------------------------------------------------------