Skip to content

Commit 5cc487e

Browse files
JacquesCaretteandreasabel
JacquesCarette
authored and
andreasabel
committed
Tighten imports some more (#2343)
* no need to use Function when only import is from Function.Base * Use Function.Base when it suffices * use Data.Product.Base as much as possible. Make imports more precise in many of the files touched. Split an example off into a README instead of using more imports just for its sake. * more tightening of imports. * a few more tightening imports
1 parent 5d687f7 commit 5cc487e

File tree

22 files changed

+118
-92
lines changed

22 files changed

+118
-92
lines changed

‎doc/README/Effect/Monad/Partiality.agda

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
-----------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Example showing the use of the partiality Monad
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --cubical-compatible --safe --guardedness #-}
8+
9+
module README.Effect.Monad.Partiality where
10+
11+
open import Codata.Musical.Notation using (♯_)
12+
open import Data.Bool.Base using (false; true)
13+
open import Data.Nat using (ℕ; _+_; _∸_; _≤?_)
14+
open import Effect.Monad.Partiality
15+
open import Relation.Nullary.Decidable using (does)
16+
17+
open Workaround
18+
19+
-- McCarthy's f91:
20+
21+
f91′ : ℕ → ℕ ⊥P
22+
f91′ n with does (n ≤? 100)
23+
... | true = later (♯ (f91′ (11 + n) >>= f91′))
24+
... | false = now (n ∸ 10)
25+
26+
f91 : ℕ → ℕ ⊥
27+
f91 n = ⟦ f91′ n ⟧P

‎src/Algebra/Module/Construct/Idealization.agda

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -43,9 +43,11 @@ import Algebra.Definitions as Definitions
4343
import Algebra.Module.Construct.DirectProduct as DirectProduct
4444
import Algebra.Module.Construct.TensorUnit as TensorUnit
4545
open import Algebra.Structures using (IsAbelianGroup; IsRing)
46-
open import Data.Product using (_,_; ∃-syntax)
46+
open import Data.Product.Base using (_,_; ∃-syntax)
4747
open import Level using (Level; _⊔_)
48-
open import Relation.Binary using (Rel; Setoid; IsEquivalence)
48+
open import Relation.Binary.Bundles using (Setoid)
49+
open import Relation.Binary.Core using (Rel)
50+
open import Relation.Binary.Structures using (IsEquivalence)
4951
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
5052

5153
------------------------------------------------------------------------

‎src/Algebra/Properties/CommutativeMonoid.agda

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

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

9-
open import Algebra.Bundles
10-
open import Algebra.Definitions
11-
open import Data.Product using (_,_; proj₂)
9+
open import Algebra.Bundles using (CommutativeMonoid)
10+
open import Algebra.Definitions using (LeftInvertible; RightInvertible; Invertible)
11+
open import Data.Product.Base using (_,_; proj₂)
1212

1313
module Algebra.Properties.CommutativeMonoid
1414
{g₁ g₂} (M : CommutativeMonoid g₁ g₂) where

‎src/Data/Container/Core.agda

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

99
module Data.Container.Core where
1010

11-
open import Level
11+
open import Level using (Level; _⊔_; suc)
1212
open import Data.Product.Base as Product using (Σ-syntax)
13-
open import Function.Base
14-
open import Function using (Inverse; _↔_)
13+
open import Function.Base using (_∘_; _∘′_)
14+
open import Function.Bundles using (Inverse; _↔_)
1515
open import Relation.Unary using (Pred; _⊆_)
1616

1717
-- Definition of Containers

‎src/Data/Container/Indexed.agda

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -11,14 +11,14 @@
1111

1212
module Data.Container.Indexed where
1313

14-
open import Level
14+
open import Level using (Level; zero; _⊔_)
1515
open import Data.Product.Base as Prod hiding (map)
16-
open import Data.W.Indexed
16+
open import Data.W.Indexed using (W)
1717
open import Function.Base renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_)
18-
open import Function using (_↔_; Inverse)
18+
open import Function.Bundles using (_↔_; Inverse)
1919
open import Relation.Unary using (Pred; _⊆_)
2020
open import Relation.Binary.Core using (Rel; REL)
21-
open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; trans; subst)
21+
open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≗_; refl; trans; subst)
2222

2323
------------------------------------------------------------------------
2424

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

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

99
module Data.Container.Indexed.Relation.Binary.Pointwise where
1010

11-
open import Data.Product using (_,_; Σ-syntax)
12-
open import Function
11+
open import Data.Product.Base using (_,_; Σ-syntax)
12+
open import Function.Base using (_∘_)
1313
open import Level using (Level; _⊔_)
1414
open import Relation.Binary using (REL; _⇒_)
15-
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
15+
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
1616

1717
open import Data.Container.Indexed.Core using (Container; Subtrees; ⟦_⟧)
1818

‎src/Data/List/Properties.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ open import Data.List.Relation.Unary.All using (All; []; _∷_)
2323
open import Data.List.Relation.Unary.Any using (Any; here; there)
2424
open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
2525
open import Data.Nat.Base
26-
open import Data.Nat.Divisibility
26+
open import Data.Nat.Divisibility using (_∣_; divides; ∣n⇒∣m*n)
2727
open import Data.Nat.Properties
2828
open import Data.Product.Base as Product
2929
using (_×_; _,_; uncurry; uncurry′; proj₁; proj₂; <_,_>)

‎src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,10 +13,10 @@ module Data.List.Relation.Ternary.Appending.Setoid.Properties
1313
where
1414

1515
open import Data.List.Base as List using (List; [])
16-
import Data.List.Properties as Listₚ
16+
import Data.List.Properties as List
1717
open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; [])
1818
import Data.List.Relation.Ternary.Appending.Properties as Appendingₚ
19-
open import Data.Product using (∃-syntax; _×_; _,_)
19+
open import Data.Product.Base using (∃-syntax; _×_; _,_)
2020
open import Function.Base using (id)
2121
open import Relation.Binary.Core using (_⇒_)
2222
open import Relation.Binary.PropositionalEquality.Core using (refl)
@@ -45,7 +45,7 @@ open Appendingₚ public
4545
++[]⁻¹ : Appending as [] cs → Pointwise _≈_ as cs
4646
++[]⁻¹ {as} {cs} ls with break ls
4747
... | cs₁ , cs₂ , refl , pw , []
48-
rewrite Listₚ.++-identityʳ cs₁
48+
rewrite List.++-identityʳ cs₁
4949
= pw
5050

5151
respʳ-≋ : ∀ {cs′} → Appending as bs cs → Pointwise _≈_ cs cs′ →

‎src/Data/List/Relation/Unary/First/Properties.agda

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

99
module Data.List.Relation.Unary.First.Properties where
1010

11-
open import Data.Empty
1211
open import Data.Fin.Base using (suc)
1312
open import Data.List.Base as List using (List; []; _∷_)
1413
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
1514
open import Data.List.Relation.Unary.Any as Any using (here; there)
1615
open import Data.List.Relation.Unary.First
1716
import Data.Sum as Sum
1817
open import Function.Base using (_∘′_; _$_; _∘_; id)
19-
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; refl; _≗_)
20-
open import Relation.Unary
21-
open import Relation.Nullary.Negation
18+
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl; _≗_)
19+
open import Relation.Unary using (Pred; _⊆_; ∁; Irrelevant; Decidable)
20+
open import Relation.Nullary.Negation using (contradiction)
2221

2322
------------------------------------------------------------------------
2423
-- map
@@ -52,7 +51,7 @@ module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
5251
module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
5352

5453
All⇒¬First : P ⊆ ∁ Q → All P ⊆ ∁ (First P Q)
55-
All⇒¬First p⇒¬q (px ∷ pxs) [ qx ] = ⊥-elim (p⇒¬q px qx)
54+
All⇒¬First p⇒¬q (px ∷ pxs) [ qx ] = contradiction qx (p⇒¬q px)
5655
All⇒¬First p⇒¬q (_ ∷ pxs) (_ ∷ hf) = All⇒¬First p⇒¬q pxs hf
5756

5857
First⇒¬All : Q ⊆ ∁ P → First P Q ⊆ ∁ (All P)
@@ -64,16 +63,16 @@ module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
6463

6564
unique-index : ∀ {xs} → P ⊆ ∁ Q → (f₁ f₂ : First P Q xs) → index f₁ ≡ index f₂
6665
unique-index p⇒¬q [ _ ] [ _ ] = refl
67-
unique-index p⇒¬q [ qx ] (px ∷ _) = ⊥-elim (p⇒¬q px qx)
68-
unique-index p⇒¬q (px ∷ _) [ qx ] = ⊥-elim (p⇒¬q px qx)
66+
unique-index p⇒¬q [ qx ] (px ∷ _) = contradiction qx (p⇒¬q px)
67+
unique-index p⇒¬q (px ∷ _) [ qx ] = contradiction qx (p⇒¬q px)
6968
unique-index p⇒¬q (_ ∷ f₁) (_ ∷ f₂) = ≡.cong suc (unique-index p⇒¬q f₁ f₂)
7069

7170
irrelevant : P ⊆ ∁ Q → Irrelevant P → Irrelevant Q → Irrelevant (First P Q)
72-
irrelevant p⇒¬q p-irr q-irr [ qx₁ ] [ qx₂ ] = ≡.cong [_] (q-irr qx₁ qx₂)
73-
irrelevant p⇒¬q p-irr q-irr [ qx₁ ] (px₂ ∷ f₂) = ⊥-elim (p⇒¬q px₂ qx₁)
74-
irrelevant p⇒¬q p-irr q-irr (px₁ ∷ f₁) [ qx₂ ] = ⊥-elim (p⇒¬q px₁ qx₂)
75-
irrelevant p⇒¬q p-irr q-irr (px₁ ∷ f₁) (px₂ ∷ f₂) =
76-
≡.cong₂ _∷_ (p-irr px₁ px₂) (irrelevant p⇒¬q p-irr q-irr f₁ f₂)
71+
irrelevant p⇒¬q p-irr q-irr [ px ] [ qx ] = ≡.cong [_] (q-irr px qx)
72+
irrelevant p⇒¬q p-irr q-irr [ qx ] (px ∷ _) = contradiction qx (p⇒¬q px)
73+
irrelevant p⇒¬q p-irr q-irr (px ∷ _) [ qx ] = contradiction qx (p⇒¬q px)
74+
irrelevant p⇒¬q p-irr q-irr (px ∷ f) (qx ∷ g) =
75+
≡.cong₂ _∷_ (p-irr px qx) (irrelevant p⇒¬q p-irr q-irr f g)
7776

7877
------------------------------------------------------------------------
7978
-- Decidability

‎src/Data/Nat/Primality/Factorisation.agda

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

99
module Data.Nat.Primality.Factorisation where
1010

11-
open import Data.Empty using (⊥-elim)
1211
open import Data.Nat.Base
1312
open import Data.Nat.Divisibility
13+
using (_∣?_; quotient; quotient>1; quotient-<; quotient-∣; m∣n⇒n≡m*quotient; _∣_; ∣1⇒≡1;
14+
divides)
1415
open import Data.Nat.Properties
1516
open import Data.Nat.Induction using (<-Rec; <-rec; <-recBuilder)
1617
open import Data.Nat.Primality
17-
open import Data.Product as Π using (∃-syntax; _×_; _,_; proj₁; proj₂)
18+
using (Prime; _Rough_; rough∧square>⇒prime; ∤⇒rough-suc; rough∧∣⇒rough; rough∧∣⇒prime;
19+
2-rough; euclidsLemma; prime⇒irreducible; ¬prime[1]; productOfPrimes≥1; prime⇒nonZero)
20+
open import Data.Product.Base using (∃-syntax; _×_; _,_; proj₁; proj₂)
1821
open import Data.List.Base using (List; []; _∷_; _++_; product)
1922
open import Data.List.Membership.Propositional using (_∈_)
2023
open import Data.List.Membership.Propositional.Properties using (∈-∃++)
2124
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
2225
open import Data.List.Relation.Unary.Any using (here; there)
2326
open import Data.List.Relation.Binary.Permutation.Propositional
2427
using (_↭_; prep; swap; ↭-reflexive; ↭-refl; ↭-trans; refl; module PermutationReasoning)
25-
open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (product-↭; All-resp-↭; shift)
28+
open import Data.List.Relation.Binary.Permutation.Propositional.Properties
29+
using (product-↭; All-resp-↭; shift)
2630
open import Data.Sum.Base using (inj₁; inj₂)
2731
open import Function.Base using (_$_; _∘_; _|>_; flip)
2832
open import Induction using (build)
2933
open import Induction.Lexicographic using (_⊗_; [_⊗_])
3034
open import Relation.Nullary.Decidable using (yes; no)
3135
open import Relation.Nullary.Negation using (contradiction)
32-
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; module ≡-Reasoning)
36+
open import Relation.Binary.PropositionalEquality
37+
using (_≡_; refl; sym; trans; cong; module ≡-Reasoning)
3338

3439
private
3540
variable

0 commit comments

Comments
 (0)