[imports] Algebra.Module.Definitions.Bi.Simultaneous .. Data.Bool.Properties (#2620)

jmougeot · web-flow · commit f8887ac046f1 · 2025-02-26T20:50:55.000Z
* Import cleanig Data

* Import cleanig Data

* fixed

* fix

* fix
diff --git a/src/Algebra/Module/Definitions/Bi/Simultaneous.agda b/src/Algebra/Module/Definitions/Bi/Simultaneous.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel)
+open import Relation.Binary.Core using (Rel)
 
 module Algebra.Module.Definitions.Bi.Simultaneous
   {a b ℓb} (A : Set a) {B : Set b} (_≈_ : Rel B ℓb)
diff --git a/src/Codata/Sized/Colist.agda b/src/Codata/Sized/Colist.agda
@@ -8,26 +8,24 @@
 
 module Codata.Sized.Colist where
 
-open import Level using (Level)
-open import Size
-open import Data.Unit.Base
-open import Data.Nat.Base
-open import Data.Product.Base using (_×_ ; _,_)
-open import Data.These.Base using (These; this; that; these)
-open import Data.Maybe.Base using (Maybe; nothing; just)
+open import Codata.Sized.Conat as Conat using (Conat ; zero ; suc)
+open import Codata.Sized.Cowriter as CW using (Cowriter; _∷_)
+open import Codata.Sized.Delay as Delay using (Delay ; now ; later)
+open import Codata.Sized.Stream using (Stream ; _∷_)
+open import Codata.Sized.Thunk using (Thunk; force)
 open import Data.List.Base using (List; []; _∷_)
 open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_)
+open import Data.Maybe.Base using (Maybe; nothing; just)
+open import Data.Nat.Base using (ℕ; suc; zero)
+open import Data.Product.Base using (_×_ ; _,_)
+open import Data.These.Base using (These; this; that; these)
+open import Data.Unit.Base using (⊤)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Data.Vec.Bounded.Base as Vec≤ using (Vec≤)
 open import Function.Base using (_$′_; _∘′_; id; _∘_)
-
-open import Codata.Sized.Thunk using (Thunk; force)
-open import Codata.Sized.Conat as Conat using (Conat ; zero ; suc)
-open import Codata.Sized.Cowriter as CW using (Cowriter; _∷_)
-open import Codata.Sized.Delay as Delay using (Delay ; now ; later)
-open import Codata.Sized.Stream using (Stream ; _∷_)
-
+open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
+open import Size using (Size; ∞)
 
 private
   variable
diff --git a/src/Codata/Sized/Conat.agda b/src/Codata/Sized/Conat.agda
@@ -8,11 +8,10 @@
 
 module Codata.Sized.Conat where
 
-open import Size
-open import Codata.Sized.Thunk
-
+open import Size using (Size ; ∞; Size<_)
+open import Codata.Sized.Thunk using (Thunk ; force)
 open import Data.Nat.Base using (ℕ ; zero ; suc)
-open import Relation.Nullary
+open import Relation.Nullary.Negation.Core using (¬_)
 
 ------------------------------------------------------------------------
 -- Definition and first values
diff --git a/src/Codata/Sized/Covec.agda b/src/Codata/Sized/Covec.agda
@@ -8,12 +8,12 @@
 
 module Codata.Sized.Covec where
 
-open import Size
-
+open import Size using (Size ; ∞)
 open import Codata.Sized.Thunk using (Thunk; force)
 open import Codata.Sized.Conat as Conat
-open import Codata.Sized.Conat.Bisimilarity
-open import Codata.Sized.Conat.Properties
+  using (Conat ; zero ; suc; _+_; infinity; fromℕ; _ℕ+_)
+open import Codata.Sized.Conat.Bisimilarity using (_⊢_≈_; zero; suc)
+open import Codata.Sized.Conat.Properties using (0ℕ+-identity)
 open import Codata.Sized.Cofin as Cofin using (Cofin; zero; suc)
 open import Codata.Sized.Colist as Colist using (Colist ; [] ; _∷_)
 open import Codata.Sized.Stream as Stream using (Stream ; _∷_)
diff --git a/src/Codata/Sized/Cowriter.agda b/src/Codata/Sized/Cowriter.agda
@@ -8,13 +8,13 @@
 
 module Codata.Sized.Cowriter where
 
-open import Size
+open import Size using (Size; ∞)
 open import Level as L using (Level)
 open import Codata.Sized.Thunk using (Thunk; force)
-open import Codata.Sized.Conat
+open import Codata.Sized.Conat using (Conat; zero; suc)
 open import Codata.Sized.Delay using (Delay; later; now)
 open import Codata.Sized.Stream as Stream using (Stream; _∷_)
-open import Data.Unit.Base
+open import Data.Unit.Base using (⊤)
 open import Data.List.Base using (List; []; _∷_)
 open import Data.List.NonEmpty.Base using (List⁺; _∷_)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
diff --git a/src/Codata/Sized/Delay.agda b/src/Codata/Sized/Delay.agda
@@ -8,18 +8,17 @@
 
 module Codata.Sized.Delay where
 
-open import Size
+open import Size using (Size; ∞)
 open import Codata.Sized.Thunk using (Thunk; force)
 open import Codata.Sized.Conat using (Conat; zero; suc; Finite)
-
-open import Data.Empty
-open import Relation.Nullary
-open import Data.Nat.Base
+open import Data.Empty using (⊥)
+open import Data.Nat.Base using (ℕ; suc; zero)
 open import Data.Maybe.Base hiding (map ; fromMaybe ; zipWith ; alignWith ; zip ; align)
 open import Data.Product.Base hiding (map ; zip)
 open import Data.Sum.Base hiding (map)
 open import Data.These.Base using (These; this; that; these)
 open import Function.Base using (id)
+open import Relation.Nullary.Negation.Core using (¬_)
 
 ------------------------------------------------------------------------
 -- Definition
diff --git a/src/Codata/Sized/M.agda b/src/Codata/Sized/M.agda
@@ -8,8 +8,8 @@
 
 module Codata.Sized.M where
 
-open import Size
-open import Level
+open import Size using (Size; ∞)
+open import Level using (Level; _⊔_)
 open import Codata.Sized.Thunk using (Thunk; force)
 open import Data.Product.Base hiding (map)
 open import Data.Container.Core as C hiding (map)
diff --git a/src/Codata/Sized/Stream.agda b/src/Codata/Sized/Stream.agda
@@ -8,17 +8,16 @@
 
 module Codata.Sized.Stream where
 
-open import Size
 open import Codata.Sized.Thunk as Thunk using (Thunk; force)
-
-open import Data.Nat.Base
+open import Data.Nat.Base using (ℕ; suc; zero)
 open import Data.List.Base using (List; []; _∷_)
 open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_; _∷⁺_)
 open import Data.Vec.Base using (Vec; []; _∷_)
 open import Data.Product.Base as P using (Σ; _×_; _,_; <_,_>; proj₁; proj₂)
 open import Function.Base using (id; _∘_)
 open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
+open import Size using (Size; ∞; Size<_)
 
 private
   variable
diff --git a/src/Codata/Sized/Stream/Bisimilarity.agda b/src/Codata/Sized/Stream/Bisimilarity.agda
@@ -8,10 +8,10 @@
 
 module Codata.Sized.Stream.Bisimilarity where
 
-open import Size
-open import Codata.Sized.Thunk
-open import Codata.Sized.Stream
-open import Level
+open import Size using (Size; ∞)
+open import Codata.Sized.Thunk using (Thunk; Thunk^R; force)
+open import Codata.Sized.Stream using (Stream; _∷_; _++_; _⁺++_)
+open import Level using (Level; _⊔_)
 open import Data.List.NonEmpty as List⁺ using (_∷_)
 open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_)
 open import Relation.Binary.Core using (Rel; REL)
diff --git a/src/Codata/Sized/Stream/Effectful.agda b/src/Codata/Sized/Stream/Effectful.agda
@@ -9,11 +9,12 @@
 module Codata.Sized.Stream.Effectful where
 
 open import Data.Product.Base using (<_,_>)
-open import Codata.Sized.Stream
-open import Effect.Functor
-open import Effect.Applicative
-open import Effect.Comonad
-open import Function.Base
+open import Codata.Sized.Stream using
+  (Stream; _∷_; _++_; _⁺++_; map; repeat; ap; head; unfold; tail)
+open import Effect.Functor using (RawFunctor)
+open import Effect.Applicative using (RawApplicative)
+open import Effect.Comonad using (RawComonad)
+open import Function.Base using (_∘′_)
 
 functor : ∀ {ℓ i} → RawFunctor {ℓ} (λ A → Stream A i)
 functor = record { _<$>_ = λ f → map f }
diff --git a/src/Codata/Sized/Stream/Instances.agda b/src/Codata/Sized/Stream/Instances.agda
@@ -8,7 +8,7 @@
 
 module Codata.Sized.Stream.Instances where
 
-open import Codata.Sized.Stream.Effectful
+open import Codata.Sized.Stream.Effectful using (functor; applicative; comonad)
 
 instance
   streamFunctor = functor
diff --git a/src/Codata/Sized/Stream/Properties.agda b/src/Codata/Sized/Stream/Properties.agda
@@ -8,25 +8,23 @@
 
 module Codata.Sized.Stream.Properties where
 
-open import Level using (Level)
-open import Size
-open import Codata.Sized.Thunk as Thunk using (Thunk; force)
-open import Codata.Sized.Stream
+open import Codata.Sized.Stream using (Stream; _∷_; _++_; map; repeat; ap;
+  lookup; splitAt; cycle; iterate; take; _⁺++_)
 open import Codata.Sized.Stream.Bisimilarity
-
-open import Data.Nat.Base
-open import Data.Nat.GeneralisedArithmetic using (fold; fold-pull)
-
+open import Codata.Sized.Thunk as Thunk using (Thunk; force)
 open import Data.List.Base as List using ([]; _∷_)
 open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_)
-import Data.List.Relation.Binary.Equality.Propositional as ≋
+open import Data.List.Relation.Binary.Equality.Propositional as ≋
+open import Data.Nat.Base using (ℕ; zero; suc; pred; _+_)
+open import Data.Nat.GeneralisedArithmetic using (fold; fold-pull)
 open import Data.Product.Base as Product using (_,_)
 open import Data.Vec.Base as Vec using (_∷_)
-
 open import Function.Base using (id; _$_; _∘′_; const)
+open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; _≢_)
 open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning)
+open import Size using (Size;  ∞)
 
 private
   variable
diff --git a/src/Codata/Sized/Thunk.agda b/src/Codata/Sized/Thunk.agda
@@ -8,8 +8,8 @@
 
 module Codata.Sized.Thunk where
 
-open import Size
-open import Relation.Unary.Sized
+open import Size using (Size; ∞; Size<_; SizedSet)
+open import Relation.Unary.Sized using (_⇒_; ∀[_])
 
 ------------------------------------------------------------------------
 -- Basic types.
diff --git a/src/Data/AVL/IndexedMap.agda b/src/Data/AVL/IndexedMap.agda
@@ -10,7 +10,7 @@ open import Data.Product.Base using (∃)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Structures using (IsStrictTotalOrder)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong; subst)
-import Data.Tree.AVL.Value
+import Data.Tree.AVL.Value using (Value)
 
 module Data.AVL.IndexedMap
   {i k v ℓ}
diff --git a/src/Data/Bool/Base.agda b/src/Data/Bool/Base.agda
@@ -9,7 +9,7 @@
 module Data.Bool.Base where
 
 open import Data.Unit.Base using (⊤)
-open import Data.Empty
+open import Data.Empty using (⊥)
 open import Level using (Level)
 
 private
diff --git a/src/Data/Bool/Instances.agda b/src/Data/Bool/Instances.agda
@@ -8,7 +8,7 @@
 
 module Data.Bool.Instances where
 
-open import Data.Bool.Properties
+open import Data.Bool.Properties using (_≟_; ≤-isDecTotalOrder)
 open import Relation.Binary.PropositionalEquality.Properties
   using (isDecEquivalence)
 
diff --git a/src/Data/Bool/ListAction.agda b/src/Data/Bool/ListAction.agda
@@ -15,7 +15,7 @@ module Data.Bool.ListAction where
 open import Data.Bool.Base using (Bool; _∧_; _∨_; true; false)
 open import Data.List.Base using (List; map; foldr)
 open import Function.Base using (_∘_)
-open import Level
+open import Level using (Level)
 
 private
   variable
diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda
@@ -7,29 +7,35 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 module Data.Bool.Properties where
-
 open import Algebra.Bundles
-open import Algebra.Lattice.Bundles
+open import Algebra.Lattice.Bundles using
+  (BooleanAlgebra; DistributiveLattice; Lattice; Semilattice)
 import Algebra.Lattice.Properties.BooleanAlgebra as BooleanAlgebraProperties
-open import Data.Bool.Base
-open import Data.Empty
-open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
-open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
+open import Data.Bool.Base using (Bool; T; _<_; _≤_; _∧_; _∨_; _xor_; b≤b; f<t;
+  f≤t; false; if_then_else_; not; true)
+open import Data.Empty using (⊥; ⊥-elim)
+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 (LeftInverse; RightInverse; Inverse)
-open import Induction.WellFounded using (WellFounded; Acc; acc)
-open import Level using (Level; 0ℓ)
+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.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
-open import Relation.Binary.PropositionalEquality.Properties
-open import Relation.Nullary.Decidable.Core using (True; yes; no; fromWitness)
-import Relation.Unary as U
+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 Algebra.Definitions {A = Bool} _≡_
 open import Algebra.Structures {A = Bool} _≡_
