Skip to content

Commit 3fad33c

Browse files
jmougeotjmougeot
authored
[Import] Codata.Sized.* (#2619)
* Codata Cleaning import 3 * Codata Cleaning import 3 * fix
1 parent 5ac10dd commit 3fad33c

File tree

10 files changed

+40
-39
lines changed

10 files changed

+40
-39
lines changed

‎src/Codata/Sized/Covec/Bisimilarity.agda

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,10 +9,10 @@
99
module Codata.Sized.Covec.Bisimilarity where
1010

1111
open import Level using (_⊔_)
12-
open import Size
13-
open import Codata.Sized.Thunk
12+
open import Size using (Size; ∞)
13+
open import Codata.Sized.Thunk using (Thunk; Thunk^R; force)
1414
open import Codata.Sized.Conat hiding (_⊔_)
15-
open import Codata.Sized.Covec
15+
open import Codata.Sized.Covec using (Covec; _∷_; [])
1616
open import Relation.Binary.Definitions
1717
using (Reflexive; Symmetric; Transitive; Sym; Trans)
1818
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)

‎src/Codata/Sized/Covec/Effectful.agda

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,10 @@
88

99
module Codata.Sized.Covec.Effectful where
1010

11-
open import Codata.Sized.Conat
12-
open import Codata.Sized.Covec
13-
open import Effect.Functor
14-
open import Effect.Applicative
11+
open import Codata.Sized.Conat using (Conat; zero; suc)
12+
open import Codata.Sized.Covec using (Covec; _∷_; []; map; replicate; ap)
13+
open import Effect.Functor using (RawFunctor)
14+
open import Effect.Applicative using (RawApplicative)
1515

1616
functor : ∀ {ℓ i n} → RawFunctor {ℓ} (λ A → Covec A n i)
1717
functor = record { _<$>_ = map }

‎src/Codata/Sized/Covec/Instances.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88

99
module Codata.Sized.Covec.Instances where
1010

11-
open import Codata.Sized.Covec.Effectful
11+
open import Codata.Sized.Covec.Effectful using (functor; applicative)
1212

1313
instance
1414
covecFunctor = functor

‎src/Codata/Sized/Covec/Properties.agda

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,13 +8,13 @@
88

99
module Codata.Sized.Covec.Properties where
1010

11-
open import Size
11+
open import Size using (Size; ∞)
1212
open import Codata.Sized.Thunk using (Thunk; force)
13-
open import Codata.Sized.Conat
14-
open import Codata.Sized.Covec
13+
open import Codata.Sized.Conat using (zero; suc)
14+
open import Codata.Sized.Covec using (Covec; _∷_; []; map)
1515
open import Codata.Sized.Covec.Bisimilarity
1616
open import Function.Base using (id; _∘_)
17-
open import Relation.Binary.PropositionalEquality.Core as ≡
17+
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
1818

1919
-- Functor laws
2020

‎src/Codata/Sized/Cowriter/Bisimilarity.agda

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -9,16 +9,16 @@
99
module Codata.Sized.Cowriter.Bisimilarity where
1010

1111
open import Level using (Level; _⊔_)
12-
open import Size
13-
open import Codata.Sized.Thunk
14-
open import Codata.Sized.Cowriter
12+
open import Size using (Size; ∞)
13+
open import Codata.Sized.Thunk using (Thunk; Thunk^R; force)
14+
open import Codata.Sized.Cowriter using (Cowriter; _∷_;[_])
1515
open import Relation.Binary.Core using (REL; Rel)
1616
open import Relation.Binary.Bundles using (Setoid)
1717
open import Relation.Binary.Structures using (IsEquivalence)
1818
open import Relation.Binary.Definitions
1919
using (Reflexive; Symmetric; Transitive; Sym; Trans)
2020
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
21-
import Relation.Binary.PropositionalEquality.Properties as ≡
21+
import Relation.Binary.PropositionalEquality.Properties as ≡ using (setoid)
2222

2323
private
2424
variable

‎src/Codata/Sized/Delay/Bisimilarity.agda

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,10 @@
88

99
module Codata.Sized.Delay.Bisimilarity where
1010

11-
open import Size
12-
open import Codata.Sized.Thunk
13-
open import Codata.Sized.Delay
14-
open import Level
11+
open import Size using (Size; ∞)
12+
open import Codata.Sized.Thunk using (Thunk; Thunk^R; force)
13+
open import Codata.Sized.Delay using (Delay; now; later)
14+
open import Level using (_⊔_)
1515
open import Relation.Binary.Definitions
1616
using (Reflexive; Symmetric; Transitive; Sym; Trans)
1717
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)

‎src/Codata/Sized/Delay/Effectful.agda

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -9,12 +9,14 @@
99
module Codata.Sized.Delay.Effectful where
1010

1111
open import Codata.Sized.Delay
12+
using (Delay; now; never; later; map; bind; zipWith; alignWith)
1213
open import Function.Base using (id)
13-
open import Effect.Choice
14-
open import Effect.Empty
15-
open import Effect.Functor
14+
open import Effect.Choice using (RawChoice)
15+
open import Effect.Empty using (RawEmpty)
16+
open import Effect.Functor using (RawFunctor)
1617
open import Effect.Applicative
17-
open import Effect.Monad
18+
using (RawApplicative; RawApplicativeZero; RawAlternative)
19+
open import Effect.Monad using (RawMonad; RawMonadZero)
1820
open import Data.These using (leftMost)
1921

2022
functor : ∀ {i ℓ} → RawFunctor {ℓ} (λ A → Delay A i)

‎src/Codata/Sized/Delay/Properties.agda

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,10 @@ open import Size
1212
import Data.Sum.Base as Sum
1313
import Data.Nat.Base as ℕ
1414
open import Codata.Sized.Thunk using (Thunk; force)
15-
open import Codata.Sized.Conat
15+
open import Codata.Sized.Conat using (Conat; zero; suc; infinity; _⊔_; toℕ)
1616
open import Codata.Sized.Conat.Bisimilarity as Coℕ using (zero ; suc)
1717
open import Codata.Sized.Delay
18-
open import Codata.Sized.Delay.Bisimilarity
18+
open import Codata.Sized.Delay.Bisimilarity using (now; later; _⊢_≈_)
1919
open import Function.Base using (id; _∘′_)
2020
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
2121

‎src/Codata/Sized/M/Bisimilarity.agda

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -8,11 +8,11 @@
88

99
module Codata.Sized.M.Bisimilarity where
1010

11-
open import Level
12-
open import Size
13-
open import Codata.Sized.Thunk
14-
open import Codata.Sized.M
15-
open import Data.Container.Core
11+
open import Level using (_⊔_)
12+
open import Size using (Size; ∞)
13+
open import Codata.Sized.Thunk using (Thunk; Thunk^R; force)
14+
open import Codata.Sized.M using (M; inf)
15+
open import Data.Container.Core using (Container)
1616
open import Data.Container.Relation.Binary.Pointwise using (Pointwise; _,_)
1717
open import Data.Product.Base using (_,_)
1818
open import Function.Base using (_∋_)

‎src/Codata/Sized/M/Properties.agda

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -8,19 +8,18 @@
88

99
module Codata.Sized.M.Properties where
1010

11-
open import Level
12-
open import Size
11+
open import Level using (_⊔_)
12+
open import Size using (Size; ∞)
1313
open import Codata.Sized.Thunk using (Thunk; force)
14-
open import Codata.Sized.M
15-
open import Codata.Sized.M.Bisimilarity
14+
open import Codata.Sized.M using (M; inf; map; unfold)
15+
open import Codata.Sized.M.Bisimilarity using (Bisim; inf)
1616
open import Data.Container.Core as C hiding (map)
17-
import Data.Container.Morphism as Mp
17+
import Data.Container.Morphism as Mp using (id; _∘_)
1818
open import Data.Product.Base as Product using (_,_)
1919
open import Data.Product.Properties hiding (map-cong)
2020
open import Function.Base using (_$′_; _∘′_)
21-
import Relation.Binary.PropositionalEquality.Core as ≡
22-
import Relation.Binary.PropositionalEquality.Properties as ≡
23-
21+
import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl; subst)
22+
import Relation.Binary.PropositionalEquality.Properties as ≡ using (setoid)
2423
open import Data.Container.Relation.Binary.Pointwise using (_,_)
2524
import Data.Container.Relation.Binary.Equality.Setoid as EqSetoid
2625

0 commit comments

Comments
 (0)