[imports] Codata.Sized.CoFin.* .. Codata.Sized.CoNat.* (#2618)

* Import Cleaning Codata 3

* bug fixed

* fixed

* fixed

* fixed

* fixed

* fix

Author: jmougeot

src/Codata/Sized/Cofin/Literals.agda

@@ -8,12 +8,12 @@
 
 module Codata.Sized.Cofin.Literals where
 
-open import Data.Nat.Base
-open import Agda.Builtin.FromNat
-open import Codata.Sized.Conat
-open import Codata.Sized.Conat.Properties
-open import Codata.Sized.Cofin
-open import Relation.Nullary.Decidable
+open import Agda.Builtin.FromNat using (Number)
+open import Data.Nat.Base using (ℕ; suc)
+open import Codata.Sized.Conat using (Conat)
+open import Codata.Sized.Conat.Properties using (_ℕ≤?_)
+open import Codata.Sized.Cofin using (Cofin; fromℕ<)
+open import Relation.Nullary.Decidable using (True; toWitness)
 
 number : ∀ n → Number (Cofin n)
 number n = record

src/Codata/Sized/Colist/Bisimilarity.agda

@@ -9,9 +9,9 @@
 module Codata.Sized.Colist.Bisimilarity where
 
 open import Level using (Level; _⊔_)
-open import Size
-open import Codata.Sized.Thunk
-open import Codata.Sized.Colist
+open import Size using (Size; ∞)
+open import Codata.Sized.Thunk using (Thunk; Thunk^R; force)
+open import Codata.Sized.Colist using (Colist; fromList; _∷_; _++_; _⁺++_; [])
 open import Data.List.Base using (List; []; _∷_)
 open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_)
 open import Data.List.NonEmpty as List⁺  using (List⁺; _∷_)

src/Codata/Sized/Colist/Effectful.agda

@@ -9,11 +9,11 @@
 module Codata.Sized.Colist.Effectful where
 
 open import Codata.Sized.Conat using (infinity)
-open import Codata.Sized.Colist
-open import Effect.Choice
-open import Effect.Empty
-open import Effect.Functor
-open import Effect.Applicative
+open import Codata.Sized.Colist using (Colist; _++_; replicate; map; ap; [])
+open import Effect.Choice using (RawChoice)
+open import Effect.Empty using (RawEmpty)
+open import Effect.Functor using (RawFunctor)
+open import Effect.Applicative using (RawApplicative; RawApplicativeZero; RawAlternative)
 
 functor : ∀ {ℓ i} → RawFunctor {ℓ} (λ A → Colist A i)
 functor = record { _<$>_ = map }

src/Codata/Sized/Colist/Properties.agda

@@ -9,29 +9,30 @@
 module Codata.Sized.Colist.Properties where
 
 open import Level using (Level)
-open import Size
+open import Size using (Size; ∞)
 open import Codata.Sized.Thunk as Thunk using (Thunk; force)
 open import Codata.Sized.Colist
 open import Codata.Sized.Colist.Bisimilarity
-open import Codata.Sized.Conat
+open import Codata.Sized.Conat using
+  (Conat; zero; suc; _+_; _⊔_; _⊓_; _∸_; fromℕ; _ℕ+_)
 open import Codata.Sized.Conat.Bisimilarity as Conat using (zero; suc)
-import Codata.Sized.Conat.Properties as Conat
+import Codata.Sized.Conat.Properties as Conat using (0∸m≈0)
 open import Codata.Sized.Cowriter as Cowriter using ([_]; _∷_)
 open import Codata.Sized.Cowriter.Bisimilarity as Cowriter using ([_]; _∷_)
 open import Codata.Sized.Stream as Stream using (Stream; _∷_)
 open import Data.Vec.Bounded as Vec≤ using (Vec≤)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_)
-import Data.List.Scans.Base as Scans
+import Data.List.Scans.Base as Scans using (scanl)
 open import Data.List.Relation.Binary.Equality.Propositional using (≋-refl)
 open import Data.Maybe.Base as Maybe using (Maybe; nothing; just)
-import Data.Maybe.Properties as Maybe
+import Data.Maybe.Properties as Maybe using (map-nothing; map-just)
 open import Data.Maybe.Relation.Unary.All using (All; nothing; just)
 open import Data.Nat.Base as ℕ using (zero; suc; z≤n; s≤s)
 open import Data.Product.Base as Product using (_×_; _,_; uncurry)
 open import Data.These.Base as These using (These; this; that; these)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
-open import Function.Base
+open import Function.Base using (const; id; _∘_; _∘′_; flip; _on_)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 
 private

src/Codata/Sized/Conat/Bisimilarity.agda

@@ -9,9 +9,9 @@
 module Codata.Sized.Conat.Bisimilarity where
 
 open import Level using (0ℓ)
-open import Size
-open import Codata.Sized.Thunk
-open import Codata.Sized.Conat
+open import Size using (Size; ∞)
+open import Codata.Sized.Thunk using (Thunk; Thunk^R; force)
+open import Codata.Sized.Conat using (Conat; zero; suc)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Structures using (IsEquivalence)
 

src/Codata/Sized/Conat/Properties.agda

@@ -8,15 +8,15 @@
 
 module Codata.Sized.Conat.Properties where
 
-open import Size
-open import Data.Nat.Base using (ℕ; zero; suc)
-open import Codata.Sized.Thunk
 open import Codata.Sized.Conat
-open import Codata.Sized.Conat.Bisimilarity
+open import Codata.Sized.Conat.Bisimilarity using (_⊢_≈_; refl; zero; suc)
+open import Codata.Sized.Thunk using (Thunk; Thunk^R; force)
+open import Data.Nat.Base using (ℕ; zero; suc)
 open import Function.Base using (_∋_)
-open import Relation.Nullary
-open import Relation.Nullary.Decidable using (map′)
 open import Relation.Binary.Definitions using (Decidable)
+open import Relation.Nullary.Decidable.Core using (yes; no; map′)
+open import Relation.Nullary.Negation.Core using (¬_)
+open import Size using (Size)
 
 private
   variable