Skip to content

Commit 7a5660f

Browse files
jmougeotjamesmckinna
jmougeot
and
jamesmckinna
authored
[Import] Data.List.Scan.* ... Data.Maybe.* (#2630)
* [Import] ... * spurious space * Update src/Data/Maybe/Instances.agda cognate grouping --------- Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
1 parent 7848967 commit 7a5660f

22 files changed

+92
-81
lines changed

‎src/Data/List/Countdown.agda‎

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -12,22 +12,20 @@ open import Relation.Binary.Bundles using (DecSetoid)
1212

1313
module Data.List.Countdown (D : DecSetoid 0ℓ 0ℓ) where
1414

15-
open import Data.Empty
15+
open import Data.Empty using (⊥; ⊥-elim)
1616
open import Data.Fin.Base using (Fin; zero; suc; punchOut)
17-
open import Data.Fin.Properties
18-
using (suc-injective; punchOut-injective)
19-
open import Function.Base
20-
open import Function.Bundles
21-
using (Injection; module Injection)
17+
open import Data.Fin.Properties using (suc-injective; punchOut-injective)
2218
open import Data.Bool.Base using (true; false)
2319
open import Data.List.Base hiding (lookup)
2420
open import Data.List.Relation.Unary.Any as Any using (here; there)
2521
open import Data.Nat.Base using (ℕ; zero; suc)
2622
open import Data.Product.Base using (∃; _,_; _×_)
27-
open import Data.Sum.Base
28-
open import Data.Sum.Properties
23+
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
24+
open import Data.Sum.Properties using (inj₁-injective; inj₂-injective)
25+
open import Function.Base using (const; _$_; _∘_)
26+
open import Function.Bundles using (Injection; module Injection)
2927
open import Relation.Nullary.Reflects using (invert)
30-
open import Relation.Nullary
28+
open import Relation.Nullary.Decidable.Core using (Dec; yes; no; _because_)
3129
open import Relation.Nullary.Decidable using (dec-true; dec-false)
3230
open import Relation.Binary.PropositionalEquality.Core as ≡
3331
using (_≡_; _≢_; refl; cong)

‎src/Data/List/Effectful.agda‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,8 @@ open import Data.Bool.Base using (false; true)
1212
open import Data.List.Base
1313
using (List; map; [_]; ap; []; _∷_; _++_; concat; concatMap)
1414
open import Data.List.Properties
15-
using (++-identityʳ; ++-assoc; map-cong; concatMap-cong; map-concatMap;
16-
concatMap-pure)
15+
using (++-identityʳ; ++-assoc; map-cong; concatMap-cong; map-concatMap
16+
; concatMap-pure)
1717
open import Effect.Choice using (RawChoice)
1818
open import Effect.Empty using (RawEmpty)
1919
open import Effect.Functor using (RawFunctor)

‎src/Data/List/Extrema.agda‎

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -11,24 +11,23 @@ open import Relation.Binary.Bundles using (TotalOrder; Setoid)
1111
module Data.List.Extrema
1212
{b ℓ₁ ℓ₂} (totalOrder : TotalOrder b ℓ₁ ℓ₂) where
1313

14-
import Algebra.Construct.NaturalChoice.Min as Min
15-
import Algebra.Construct.NaturalChoice.Max as Max
1614
open import Data.List.Base using (List; foldr)
1715
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
18-
open import Data.List.Relation.Unary.All using (All; []; _∷_; lookup; map; tabulate)
16+
open import Data.List.Relation.Unary.All
17+
using (All; []; _∷_; lookup; map; tabulate)
1918
open import Data.List.Membership.Propositional using (_∈_; lose)
2019
open import Data.List.Membership.Propositional.Properties
2120
using (foldr-selective)
2221
open import Data.List.Relation.Binary.Subset.Propositional using (_⊆_; _⊇_)
23-
open import Data.List.Properties
22+
open import Data.List.Properties as List
23+
using (foldr-preservesᵒ; foldr-preservesᵇ; foldr-forcesᵇ)
2424
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
2525
open import Function.Base using (id; flip; _on_; _∘_)
2626
open import Level using (Level)
2727
open import Relation.Unary using (Pred)
2828
import Relation.Binary.Construct.NonStrictToStrict as NonStrictToStrict
2929
open import Relation.Binary.PropositionalEquality.Core
3030
using (_≡_; sym; subst) renaming (refl to ≡-refl)
31-
import Relation.Binary.Construct.On as On
3231

3332
------------------------------------------------------------------------
3433
-- Setup

‎src/Data/List/Fresh.agda‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -25,8 +25,9 @@ open import Function.Base using (_∘′_; flip; id; _on_)
2525
open import Relation.Nullary using (does)
2626
open import Relation.Unary as U using (Pred)
2727
open import Relation.Binary.Core using (Rel)
28-
import Relation.Binary.Definitions as B
29-
open import Relation.Nary using (∀[_]; _⇒_)
28+
import Relation.Binary.Definitions as B using (Reflexive)
29+
open import Relation.Nary using (_⇒_; ∀[_])
30+
3031

3132
private
3233
variable

‎src/Data/List/Instances.agda‎

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

99
module Data.List.Instances where
1010

11-
open import Data.List.Base
11+
open import Data.List.Base using (List; []; _∷_)
1212
open import Data.List.Effectful
13+
using (functor; applicative; applicativeZero; alternative; monad
14+
; monadZero; monadPlus)
1315
import Data.List.Effectful.Transformer as Trans
16+
using (functor; applicative; monad; monadT)
1417
open import Data.List.Properties
1518
using (≡-dec)
1619
open import Data.List.Relation.Binary.Pointwise
1720
using (Pointwise)
1821
open import Data.List.Relation.Binary.Lex.NonStrict
1922
using (Lex-≤; ≤-isDecTotalOrder)
20-
open import Level
21-
open import Relation.Binary.Core
22-
open import Relation.Binary.PropositionalEquality.Core
23+
open import Level using (Level)
24+
open import Relation.Binary.Core using (Rel)
25+
open import Relation.Binary.PropositionalEquality.Core using (_≡_)
2326
open import Relation.Binary.PropositionalEquality.Properties
2427
using (isDecEquivalence)
2528
open import Relation.Binary.TypeClasses
29+
using (IsDecTotalOrder; IsDecEquivalence; _≟_)
2630

2731
private
2832
variable

‎src/Data/List/Properties.agda‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@
1212

1313
module Data.List.Properties where
1414

15-
open import Algebra.Bundles
15+
open import Algebra.Bundles using (Semigroup; Monoid)
1616
open import Algebra.Consequences.Propositional
1717
using (selfInverse⇒involutive; selfInverse⇒injective)
1818
open import Algebra.Definitions as AlgebraicDefinitions using (SelfInverse; Involutive)
@@ -42,8 +42,10 @@ open import Relation.Binary.PropositionalEquality.Core as ≡
4242
open import Relation.Binary.PropositionalEquality.Properties as ≡
4343
open import Relation.Binary.Core using (Rel)
4444
open import Relation.Nullary.Reflects using (invert)
45-
open import Relation.Nullary using (¬_; Dec; does; _because_; yes; no; contradiction)
46-
open import Relation.Nullary.Decidable as Decidable using (isYes; map′; ⌊_⌋; ¬?; _×-dec_; dec-true; dec-false)
45+
open import Relation.Nullary.Decidable.Core using (Dec; yes; no; _because_; does)
46+
open import Relation.Nullary.Negation.Core using (contradiction; ¬_)
47+
open import Relation.Nullary.Decidable as Decidable
48+
using (isYes; map′; ⌊_⌋; ¬?; _×-dec_; dec-true; dec-false)
4749
open import Relation.Unary using (Pred; Decidable; ∁; _≐_)
4850
open import Relation.Unary.Properties using (∁?)
4951
import Data.Nat.GeneralisedArithmetic as ℕ

‎src/Data/List/Reflection.agda‎

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

99
module Data.List.Reflection where
1010

11-
open import Data.List.Base
12-
open import Reflection.AST.Term
13-
open import Reflection.AST.Argument
11+
open import Data.List.Base using (List; []; _∷_)
12+
open import Reflection.AST.Term using (Term; def; con; _⋯⟅∷⟆_)
13+
open import Reflection.AST.Argument using (Arg; _⟨∷⟩_)
1414

1515
------------------------------------------------------------------------
1616
-- Type

‎src/Data/List/Scans/Properties.agda‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,8 @@ module Data.List.Scans.Properties where
1010

1111
open import Data.List.Base as List using (List; []; _∷_)
1212
open import Data.List.NonEmpty.Base as List⁺ using (List⁺; _∷_; toList)
13-
import Data.List.Properties as List
14-
import Data.List.NonEmpty.Properties as List⁺
15-
open import Data.List.Scans.Base
13+
import Data.List.Properties as List using (map-∘)
14+
open import Data.List.Scans.Base using (scanr⁺; scanr; scanl⁺; scanl)
1615
open import Function.Base using (_∘_; _$_)
1716
open import Level using (Level)
1817
open import Relation.Binary.PropositionalEquality.Core

‎src/Data/List/Sort.agda‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,13 +9,14 @@
99

1010
{-# OPTIONS --cubical-compatible --safe #-}
1111

12-
open import Data.List.Base using (List)
1312
open import Relation.Binary.Bundles using (DecTotalOrder)
1413

1514
module Data.List.Sort
1615
{a ℓ₁ ℓ₂} (O : DecTotalOrder a ℓ₁ ℓ₂)
1716
where
1817

18+
open import Data.List.Base using (List)
19+
1920
open DecTotalOrder O renaming (Carrier to A)
2021

2122
------------------------------------------------------------------------

‎src/Data/List/Sort/Base.agda‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,15 +6,16 @@
66

77
{-# OPTIONS --cubical-compatible --safe #-}
88

9-
open import Data.List.Base using (List)
10-
open import Data.List.Relation.Binary.Permutation.Propositional
11-
open import Level using (_⊔_)
129
open import Relation.Binary.Bundles using (TotalOrder)
1310

1411
module Data.List.Sort.Base
1512
{a ℓ₁ ℓ₂} (totalOrder : TotalOrder a ℓ₁ ℓ₂)
1613
where
1714

15+
open import Data.List.Base using (List)
16+
open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_)
17+
open import Level using (_⊔_)
18+
1819
open TotalOrder totalOrder renaming (Carrier to A)
1920
open import Data.List.Relation.Unary.Sorted.TotalOrder totalOrder
2021

0 commit comments

Comments
 (0)