From 850664ac188b6d4a75c4808d9bdde4e15a6186eb Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Sat, 24 Jun 2023 13:36:00 -0400 Subject: [PATCH] Cut down `Function` imports --- src/Algebra/Construct/NaturalChoice/Min.agda | 2 +- src/Algebra/Morphism.agda | 2 +- src/Algebra/Ordered/Structures.agda | 2 +- src/Algebra/Solver/Ring/AlmostCommutativeRing.agda | 2 +- src/Data/Container/Combinator.agda | 2 +- src/Data/Container/Combinator/Properties.agda | 2 +- src/Data/Container/Indexed/Combinator.agda | 2 +- src/Data/Container/Indexed/FreeMonad.agda | 2 +- src/Data/Container/Indexed/WithK.agda | 2 +- src/Data/Container/Morphism.agda | 2 +- src/Data/Container/Morphism/Properties.agda | 2 +- src/Data/Container/Properties.agda | 2 +- src/Data/Container/Relation/Unary/All.agda | 2 +- src/Data/Digit/Properties.agda | 2 +- src/Data/Fin/Permutation/Transposition/List.agda | 2 +- src/Data/Fin/Substitution/Lemmas.agda | 6 +++--- src/Data/Fin/Substitution/List.agda | 2 +- src/Data/Float/Properties.agda | 2 +- src/Data/List/Relation/Unary/Grouped/Properties.agda | 3 ++- src/Data/Nat/Binary/Subtraction.agda | 2 +- src/Data/Nat/DivMod.agda | 2 +- src/Data/Nat/Show/Properties.agda | 2 +- src/Data/Parity/Properties.agda | 3 ++- src/Data/Sign/Properties.agda | 3 ++- src/Data/Star/Environment.agda | 2 +- src/Data/Tree/AVL/Value.agda | 2 +- src/Data/Tree/Binary/Properties.agda | 2 +- src/Data/Trie/NonEmpty.agda | 2 +- src/Data/Vec/Effectful.agda | 2 +- src/Data/Vec/Relation/Binary/Lex/NonStrict.agda | 2 +- src/Data/Vec/Relation/Unary/AllPairs.agda | 2 +- src/Data/Vec/Relation/Unary/AllPairs/Properties.agda | 2 +- src/Function/Injection.agda | 2 +- src/Function/Metric/Nat/Bundles.agda | 2 +- src/Function/Metric/Nat/Structures.agda | 2 +- src/Function/Metric/Rational/Bundles.agda | 2 +- src/Function/Metric/Rational/Structures.agda | 2 +- src/Function/Reasoning.agda | 2 +- src/Reflection/AST/Meta.agda | 4 ++-- src/Reflection/AST/Name.agda | 8 ++++---- src/Reflection/AST/Traversal.agda | 12 ++++++------ src/Reflection/External.agda | 2 +- src/Relation/Binary/OrderMorphism.agda | 2 +- src/Relation/Unary/Algebra.agda | 2 +- src/Tactic/Cong.agda | 2 +- .../RingSolver/Core/AlmostCommutativeRing.agda | 2 +- tests/data/appending/Main.agda | 2 +- tests/data/colist/Main.agda | 2 +- 48 files changed, 62 insertions(+), 59 deletions(-) diff --git a/src/Algebra/Construct/NaturalChoice/Min.agda b/src/Algebra/Construct/NaturalChoice/Min.agda index 1184f4fe30..89bd2eefb8 100644 --- a/src/Algebra/Construct/NaturalChoice/Min.agda +++ b/src/Algebra/Construct/NaturalChoice/Min.agda @@ -11,7 +11,7 @@ open import Algebra.Bundles open import Algebra.Construct.NaturalChoice.Base open import Data.Sum using (inj₁; inj₂; [_,_]) open import Data.Product using (_,_) -open import Function using (id) +open import Function.Base using (id) open import Relation.Binary import Algebra.Construct.NaturalChoice.MinOp as MinOp diff --git a/src/Algebra/Morphism.agda b/src/Algebra/Morphism.agda index fbcb2b0d12..59a6f22e23 100644 --- a/src/Algebra/Morphism.agda +++ b/src/Algebra/Morphism.agda @@ -11,7 +11,7 @@ module Algebra.Morphism where import Algebra.Morphism.Definitions as MorphismDefinitions open import Algebra import Algebra.Properties.Group as GroupP -open import Function hiding (Morphism) +open import Function.Base open import Level open import Relation.Binary import Relation.Binary.Reasoning.Setoid as EqR diff --git a/src/Algebra/Ordered/Structures.agda b/src/Algebra/Ordered/Structures.agda index 1c46f007f7..ab211cc497 100644 --- a/src/Algebra/Ordered/Structures.agda +++ b/src/Algebra/Ordered/Structures.agda @@ -22,7 +22,7 @@ open import Algebra.Core open import Algebra.Definitions _≈_ open import Algebra.Structures _≈_ open import Data.Product using (proj₁; proj₂) -open import Function using (flip) +open import Function.Base using (flip) open import Level using (_⊔_) open import Relation.Binary.Definitions using (Transitive; Monotonic₁; Monotonic₂) open import Relation.Binary.Structures using (IsPreorder; IsPartialOrder) diff --git a/src/Algebra/Solver/Ring/AlmostCommutativeRing.agda b/src/Algebra/Solver/Ring/AlmostCommutativeRing.agda index 47cda5c4f9..2bcfe92901 100644 --- a/src/Algebra/Solver/Ring/AlmostCommutativeRing.agda +++ b/src/Algebra/Solver/Ring/AlmostCommutativeRing.agda @@ -14,7 +14,7 @@ open import Algebra.Structures open import Algebra.Definitions import Algebra.Morphism as Morphism import Algebra.Morphism.Definitions as MorphismDefinitions -open import Function hiding (Morphism) +open import Function.Base using (id) open import Level open import Relation.Binary diff --git a/src/Data/Container/Combinator.agda b/src/Data/Container/Combinator.agda index e70d3e5ef4..c68536427b 100644 --- a/src/Data/Container/Combinator.agda +++ b/src/Data/Container/Combinator.agda @@ -13,7 +13,7 @@ open import Data.Empty.Polymorphic using (⊥; ⊥-elim) open import Data.Product as P using (_,_; <_,_>; proj₁; proj₂; ∃) open import Data.Sum.Base as S using ([_,_]′) open import Data.Unit.Polymorphic.Base using (⊤) -import Function as F +import Function.Base as F open import Data.Container.Core open import Data.Container.Relation.Unary.Any diff --git a/src/Data/Container/Combinator/Properties.agda b/src/Data/Container/Combinator/Properties.agda index 5799b857f8..b93d6c7a7a 100644 --- a/src/Data/Container/Combinator/Properties.agda +++ b/src/Data/Container/Combinator/Properties.agda @@ -15,7 +15,7 @@ open import Data.Container.Relation.Unary.Any open import Data.Empty using (⊥-elim) open import Data.Product as Prod using (∃; _,_; proj₁; proj₂; <_,_>; uncurry; curry) open import Data.Sum.Base as S using (inj₁; inj₂; [_,_]′; [_,_]) -open import Function as F using (_∘′_) +open import Function.Base as F using (_∘′_) open import Function.Inverse as Inv using (_↔_; inverse; module Inverse) open import Level using (_⊔_; lower) open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_) diff --git a/src/Data/Container/Indexed/Combinator.agda b/src/Data/Container/Indexed/Combinator.agda index 78e5d213d2..bc99e83f96 100644 --- a/src/Data/Container/Indexed/Combinator.agda +++ b/src/Data/Container/Indexed/Combinator.agda @@ -15,7 +15,7 @@ open import Data.Unit.Polymorphic.Base using (⊤) open import Data.Product as Prod hiding (Σ) renaming (_×_ to _⟨×⟩_) open import Data.Sum renaming (_⊎_ to _⟨⊎⟩_) open import Data.Sum.Relation.Unary.All as All using (All) -open import Function as F hiding (id; const) renaming (_∘_ to _⟨∘⟩_) +open import Function.Base as F hiding (id; const) renaming (_∘_ to _⟨∘⟩_) open import Function.Inverse using (_↔̇_; inverse) open import Level open import Relation.Unary using (Pred; _⊆_; _∪_; _∩_; ⋃; ⋂) diff --git a/src/Data/Container/Indexed/FreeMonad.agda b/src/Data/Container/Indexed/FreeMonad.agda index 1f7d63428d..f2fe0d2aab 100644 --- a/src/Data/Container/Indexed/FreeMonad.agda +++ b/src/Data/Container/Indexed/FreeMonad.agda @@ -9,7 +9,7 @@ module Data.Container.Indexed.FreeMonad where open import Level -open import Function hiding (const) +open import Function.Base hiding (const) open import Effect.Monad.Predicate open import Data.Container.Indexed open import Data.Container.Indexed.Combinator hiding (id; _∘_) diff --git a/src/Data/Container/Indexed/WithK.agda b/src/Data/Container/Indexed/WithK.agda index 2e1a7b7426..565b14fcdd 100644 --- a/src/Data/Container/Indexed/WithK.agda +++ b/src/Data/Container/Indexed/WithK.agda @@ -16,7 +16,7 @@ module Data.Container.Indexed.WithK where open import Axiom.Extensionality.Heterogeneous using (Extensionality) open import Data.Container.Indexed hiding (module PlainMorphism) open import Data.Product as Prod hiding (map) -open import Function renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_) +open import Function.Base renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_) open import Level open import Relation.Unary using (Pred; _⊆_) open import Relation.Binary.PropositionalEquality as P using (_≡_; refl) diff --git a/src/Data/Container/Morphism.agda b/src/Data/Container/Morphism.agda index 6494e5a3b8..0e26d48199 100644 --- a/src/Data/Container/Morphism.agda +++ b/src/Data/Container/Morphism.agda @@ -9,7 +9,7 @@ module Data.Container.Morphism where open import Data.Container.Core -import Function as F +import Function.Base as F module _ {s p} (C : Container s p) where diff --git a/src/Data/Container/Morphism/Properties.agda b/src/Data/Container/Morphism/Properties.agda index 16b3dd9333..0859cfe0be 100644 --- a/src/Data/Container/Morphism/Properties.agda +++ b/src/Data/Container/Morphism/Properties.agda @@ -9,7 +9,7 @@ module Data.Container.Morphism.Properties where open import Level using (_⊔_; suc) -open import Function as F using (_$_) +open import Function.Base as F using (_$_) open import Data.Product using (∃; proj₁; proj₂; _,_) open import Relation.Binary using (Setoid) open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_) diff --git a/src/Data/Container/Properties.agda b/src/Data/Container/Properties.agda index 193f7cf702..9ee24ad878 100644 --- a/src/Data/Container/Properties.agda +++ b/src/Data/Container/Properties.agda @@ -8,7 +8,7 @@ module Data.Container.Properties where -import Function as F +import Function.Base as F open import Relation.Binary open import Data.Container.Core diff --git a/src/Data/Container/Relation/Unary/All.agda b/src/Data/Container/Relation/Unary/All.agda index 2a6f858c87..65d593eea4 100644 --- a/src/Data/Container/Relation/Unary/All.agda +++ b/src/Data/Container/Relation/Unary/All.agda @@ -11,7 +11,7 @@ module Data.Container.Relation.Unary.All where open import Level using (_⊔_) open import Relation.Unary using (Pred; _⊆_) open import Data.Product as Prod using (_,_; proj₁; proj₂; ∃) -open import Function as F +open import Function.Base using (_∘′_; id) open import Data.Container.Core hiding (map) import Data.Container.Morphism as M diff --git a/src/Data/Digit/Properties.agda b/src/Data/Digit/Properties.agda index 0ba2cab34f..355467ec39 100644 --- a/src/Data/Digit/Properties.agda +++ b/src/Data/Digit/Properties.agda @@ -17,7 +17,7 @@ import Data.Vec.Relation.Unary.Unique.Propositional.Properties as Uniqueₚ open import Data.Vec.Relation.Unary.AllPairs using (allPairs?) open import Relation.Nullary.Decidable using (True; from-yes; ¬?) open import Relation.Binary.PropositionalEquality as P using (_≡_; refl) -open import Function using (_∘_) +open import Function.Base using (_∘_) module Data.Digit.Properties where diff --git a/src/Data/Fin/Permutation/Transposition/List.agda b/src/Data/Fin/Permutation/Transposition/List.agda index 42505de541..4ed0583372 100644 --- a/src/Data/Fin/Permutation/Transposition/List.agda +++ b/src/Data/Fin/Permutation/Transposition/List.agda @@ -15,7 +15,7 @@ import Data.Fin.Permutation.Components as PC open import Data.List using (List; []; _∷_; map) open import Data.Nat.Base using (ℕ; suc; zero) open import Data.Product using (_×_; _,_) -open import Function using (_∘_) +open import Function.Base using (_∘_) open import Relation.Binary.PropositionalEquality using (_≡_; sym; cong; module ≡-Reasoning) open ≡-Reasoning diff --git a/src/Data/Fin/Substitution/Lemmas.agda b/src/Data/Fin/Substitution/Lemmas.agda index 018ed86f29..3747f21018 100644 --- a/src/Data/Fin/Substitution/Lemmas.agda +++ b/src/Data/Fin/Substitution/Lemmas.agda @@ -14,7 +14,7 @@ open import Data.Nat hiding (_⊔_; _/_) open import Data.Fin.Base using (Fin; zero; suc; lift) open import Data.Vec.Base import Data.Vec.Properties as VecProp -open import Function as Fun using (_∘_; _$_) +open import Function.Base as Fun using (_∘_; _$_; flip) open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl; sym; cong; cong₂) open import Relation.Binary.Construct.Closure.ReflexiveTransitive @@ -222,7 +222,7 @@ record Lemmas₃ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where ∀ k t → t /✶ ρs₁ ↑✶ k ≡ t /✶ ρs₂ ↑✶ k /✶-↑✶′ ρs₁ ρs₂ hyp = /✶-↑✶ ρs₁ ρs₂ (λ k x → begin var x /✶ ρs₁ ↑✶ k ≡⟨ sym (lookup-⨀ x (ρs₁ ↑✶ k)) ⟩ - lookup (⨀ (ρs₁ ↑✶ k)) x ≡⟨ cong (Fun.flip lookup x) (hyp k) ⟩ + lookup (⨀ (ρs₁ ↑✶ k)) x ≡⟨ cong (flip lookup x) (hyp k) ⟩ lookup (⨀ (ρs₂ ↑✶ k)) x ≡⟨ lookup-⨀ x (ρs₂ ↑✶ k) ⟩ var x /✶ ρs₂ ↑✶ k ∎) @@ -341,7 +341,7 @@ record Lemmas₄ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where var (suc x) / ρ ↑ ≡ var x / ρ / wk suc-/-↑ {ρ = ρ} x = begin var (suc x) / ρ ↑ ≡⟨ var-/ ⟩ - lookup (map weaken ρ) x ≡⟨ cong (Fun.flip lookup x) (map-weaken {ρ = ρ}) ⟩ + lookup (map weaken ρ) x ≡⟨ cong (flip lookup x) (map-weaken {ρ = ρ}) ⟩ lookup (ρ ⊙ wk) x ≡⟨ lookup-⊙ x {ρ₁ = ρ} ⟩ lookup ρ x / wk ≡⟨ cong₂ _/_ (sym var-/) refl ⟩ var x / ρ / wk ∎ diff --git a/src/Data/Fin/Substitution/List.agda b/src/Data/Fin/Substitution/List.agda index 8927b3b21f..63a7e39279 100644 --- a/src/Data/Fin/Substitution/List.agda +++ b/src/Data/Fin/Substitution/List.agda @@ -17,7 +17,7 @@ module Data.Fin.Substitution.List {ℓ} {T : ℕ → Set ℓ} (lemmas₄ : Lemma open import Data.List.Base open import Data.List.Properties open import Data.Fin.Substitution -import Function as Fun +import Function.Base as Fun open import Relation.Binary.PropositionalEquality open ≡-Reasoning diff --git a/src/Data/Float/Properties.agda b/src/Data/Float/Properties.agda index b2b2fc2c9e..b2caebb616 100644 --- a/src/Data/Float/Properties.agda +++ b/src/Data/Float/Properties.agda @@ -15,7 +15,7 @@ import Data.Maybe.Properties as Mₚ import Data.Nat.Properties as Nₚ import Data.Word.Base as Word import Data.Word.Properties as Wₚ -open import Function using (_∘_) +open import Function.Base using (_∘_) open import Relation.Nullary.Decidable as RN using (map′) open import Relation.Binary import Relation.Binary.Construct.On as On diff --git a/src/Data/List/Relation/Unary/Grouped/Properties.agda b/src/Data/List/Relation/Unary/Grouped/Properties.agda index 189dba033c..a8a72e6cec 100644 --- a/src/Data/List/Relation/Unary/Grouped/Properties.agda +++ b/src/Data/List/Relation/Unary/Grouped/Properties.agda @@ -14,7 +14,8 @@ open import Data.List.Relation.Unary.All as All using (All; []; _∷_) import Data.List.Relation.Unary.All.Properties as All open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_) open import Data.List.Relation.Unary.Grouped -open import Function using (_∘_; _⇔_; Equivalence) +open import Function.Base using (_∘_) +open import Function.Bundles using (module Equivalence; _⇔_) open import Relation.Binary as B using (REL; Rel) open import Relation.Unary as U using (Pred) open import Relation.Nullary using (¬_; does; yes; no) diff --git a/src/Data/Nat/Binary/Subtraction.agda b/src/Data/Nat/Binary/Subtraction.agda index 67eebc88f6..8b095b137f 100644 --- a/src/Data/Nat/Binary/Subtraction.agda +++ b/src/Data/Nat/Binary/Subtraction.agda @@ -19,7 +19,7 @@ import Data.Nat.Properties as ℕₚ open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃) open import Data.Sum using (inj₁; inj₂) open import Data.Vec using ([]; _∷_) -open import Function using (_∘_; _$_) +open import Function.Base using (_∘_; _$_) open import Level using (0ℓ) open import Relation.Binary using (Tri; tri<; tri≈; tri>; _Preserves_⟶_; _Preserves₂_⟶_⟶_) diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda index f2b2d8657e..b4c225d6a4 100644 --- a/src/Data/Nat/DivMod.agda +++ b/src/Data/Nat/DivMod.agda @@ -17,7 +17,7 @@ open import Data.Nat.DivMod.Core open import Data.Nat.Divisibility.Core open import Data.Nat.Induction open import Data.Nat.Properties -open import Function using (_$_) +open import Function.Base using (_$_) open import Relation.Binary.PropositionalEquality open import Relation.Nullary.Decidable using (yes; no) open import Relation.Nullary.Decidable using (False; toWitnessFalse) diff --git a/src/Data/Nat/Show/Properties.agda b/src/Data/Nat/Show/Properties.agda index 739a00c2e4..87622b79bf 100644 --- a/src/Data/Nat/Show/Properties.agda +++ b/src/Data/Nat/Show/Properties.agda @@ -8,7 +8,7 @@ open import Data.Digit using (showDigit; toDigits) open import Data.Digit.Properties using (toDigits-injective; showDigit-injective) -open import Function using (_∘_) +open import Function.Base using (_∘_) import Data.List.Properties as Listₚ open import Data.Nat.Base using (ℕ) open import Data.Nat.Properties using (_≤?_) diff --git a/src/Data/Parity/Properties.agda b/src/Data/Parity/Properties.agda index ed25a7b2fe..b9fb8a5eb7 100644 --- a/src/Data/Parity/Properties.agda +++ b/src/Data/Parity/Properties.agda @@ -14,7 +14,8 @@ open import Data.Nat.Base as ℕ using (zero; suc; parity) open import Data.Parity.Base as ℙ using (Parity; 0ℙ; 1ℙ; _⁻¹; toSign; fromSign) open import Data.Product using (_,_) open import Data.Sign.Base as 𝕊 -open import Function hiding (Inverse) +open import Function.Base using (_$_; id) +open import Function.Definitions using (Injective; Surjective) open import Level using (0ℓ) open import Relation.Binary using (Decidable; DecidableEquality; Setoid; DecSetoid; IsDecEquivalence) diff --git a/src/Data/Sign/Properties.agda b/src/Data/Sign/Properties.agda index ccaa33f0d1..5ca9a36e95 100644 --- a/src/Data/Sign/Properties.agda +++ b/src/Data/Sign/Properties.agda @@ -12,7 +12,8 @@ open import Algebra.Bundles open import Data.Empty open import Data.Sign.Base open import Data.Product using (_,_) -open import Function hiding (Inverse) +open import Function.Base using (_$_; id) +open import Function.Definitions using (Injective) open import Level using (0ℓ) open import Relation.Binary using (Decidable; DecidableEquality; Setoid; DecSetoid; IsDecEquivalence) diff --git a/src/Data/Star/Environment.agda b/src/Data/Star/Environment.agda index 65fcbd4818..c7ccb18ef4 100644 --- a/src/Data/Star/Environment.agda +++ b/src/Data/Star/Environment.agda @@ -13,7 +13,7 @@ open import Data.Star.List open import Data.Star.Decoration open import Data.Star.Pointer as Pointer hiding (lookup) open import Data.Unit -open import Function hiding (_∋_) +open import Function.Base hiding (_∋_) open import Relation.Binary.PropositionalEquality open import Relation.Binary.Construct.Closure.ReflexiveTransitive diff --git a/src/Data/Tree/AVL/Value.agda b/src/Data/Tree/AVL/Value.agda index 91633bfb6d..4f8543b6ba 100644 --- a/src/Data/Tree/AVL/Value.agda +++ b/src/Data/Tree/AVL/Value.agda @@ -13,7 +13,7 @@ module Data.Tree.AVL.Value {a ℓ} (S : Setoid a ℓ) where open import Data.Product using (Σ; _,_) open import Level using (suc; _⊔_) -import Function as F +import Function.Base as F open Setoid S renaming (Carrier to Key) ----------------------------------------------------------------------- diff --git a/src/Data/Tree/Binary/Properties.agda b/src/Data/Tree/Binary/Properties.agda index c3dc189f8d..b523b1e6f1 100644 --- a/src/Data/Tree/Binary/Properties.agda +++ b/src/Data/Tree/Binary/Properties.agda @@ -8,7 +8,7 @@ module Data.Tree.Binary.Properties where -open import Function using (_∘_) +open import Function.Base using (_∘_) open import Function.Nary.NonDependent using (congₙ) open import Level using (Level) open import Data.Nat.Base using (suc; _+_) diff --git a/src/Data/Trie/NonEmpty.agda b/src/Data/Trie/NonEmpty.agda index 6de3c53313..118a0db1bd 100644 --- a/src/Data/Trie/NonEmpty.agda +++ b/src/Data/Trie/NonEmpty.agda @@ -18,7 +18,7 @@ open import Data.List.Base as List using (List; []; _∷_; _++_) open import Data.List.NonEmpty as List⁺ using (List⁺; [_]; concatMap) open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′) hiding (module Maybe) open import Data.These as These using (These; this; that; these) -open import Function as F +open import Function.Base as F import Function.Identity.Effectful as Identity open import Relation.Unary using (_⇒_; IUniversal) diff --git a/src/Data/Vec/Effectful.agda b/src/Data/Vec/Effectful.agda index aa1f6dcba7..5d8e438537 100644 --- a/src/Data/Vec/Effectful.agda +++ b/src/Data/Vec/Effectful.agda @@ -16,7 +16,7 @@ open import Effect.Applicative as App using (RawApplicative) open import Effect.Functor as Fun using (RawFunctor) open import Effect.Monad using (RawMonad; RawMonadT; mkRawMonad) import Function.Identity.Effectful as Id -open import Function hiding (Morphism) +open import Function.Base open import Level using (Level) private diff --git a/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda b/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda index 409732dc0b..877d345045 100644 --- a/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda +++ b/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda @@ -19,7 +19,7 @@ open import Data.Vec using (Vec; []; _∷_) import Data.Vec.Relation.Binary.Lex.Strict as Strict open import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise using (Pointwise; []; _∷_; head; tail) -open import Function using (id) +open import Function.Base using (id) open import Relation.Binary import Relation.Binary.Construct.NonStrictToStrict as Conv open import Relation.Binary.PropositionalEquality as P using (_≡_) diff --git a/src/Data/Vec/Relation/Unary/AllPairs.agda b/src/Data/Vec/Relation/Unary/AllPairs.agda index 7c3eabcb83..0fee880769 100644 --- a/src/Data/Vec/Relation/Unary/AllPairs.agda +++ b/src/Data/Vec/Relation/Unary/AllPairs.agda @@ -15,7 +15,7 @@ open import Data.Nat.Base using (suc) open import Data.Vec.Base as Vec using (Vec; []; _∷_) open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_) open import Data.Product as Prod using (_,_; _×_; uncurry; <_,_>) -open import Function using (id; _∘_) +open import Function.Base using (id; _∘_) open import Level using (_⊔_) open import Relation.Binary as B using (Rel; _⇒_) open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_) diff --git a/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda b/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda index 7876928cc7..339a884a3b 100644 --- a/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda +++ b/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda @@ -17,7 +17,7 @@ open import Data.Bool.Base using (true; false) open import Data.Fin.Base using (Fin) open import Data.Fin.Properties using (suc-injective) open import Data.Nat.Base using (zero; suc; _+_) -open import Function using (_∘_) +open import Function.Base using (_∘_) open import Level using (Level) open import Relation.Binary using (Rel) open import Relation.Binary.PropositionalEquality using (_≢_) diff --git a/src/Function/Injection.agda b/src/Function/Injection.agda index bfa03a1ff1..4f746c2beb 100644 --- a/src/Function/Injection.agda +++ b/src/Function/Injection.agda @@ -13,7 +13,7 @@ module Function.Injection where -open import Function as Fun using () renaming (_∘_ to _⟨∘⟩_) +open import Function.Base as Fun using () renaming (_∘_ to _⟨∘⟩_) open import Level open import Relation.Binary open import Function.Equality as F diff --git a/src/Function/Metric/Nat/Bundles.agda b/src/Function/Metric/Nat/Bundles.agda index e0983246eb..57ff945ee0 100644 --- a/src/Function/Metric/Nat/Bundles.agda +++ b/src/Function/Metric/Nat/Bundles.agda @@ -13,7 +13,7 @@ module Function.Metric.Nat.Bundles where open import Data.Nat.Base hiding (suc; _⊔_) -open import Function using (const) +open import Function.Base using (const) open import Level using (Level; suc; _⊔_) open import Relation.Binary.Core open import Relation.Binary.PropositionalEquality diff --git a/src/Function/Metric/Nat/Structures.agda b/src/Function/Metric/Nat/Structures.agda index d601cad35f..648e7a4adc 100644 --- a/src/Function/Metric/Nat/Structures.agda +++ b/src/Function/Metric/Nat/Structures.agda @@ -9,7 +9,7 @@ module Function.Metric.Nat.Structures where open import Data.Nat.Base hiding (suc) -open import Function using (const) +open import Function.Base using (const) open import Level using (Level; suc) open import Relation.Binary hiding (Symmetric) open import Relation.Binary.PropositionalEquality using (_≡_) diff --git a/src/Function/Metric/Rational/Bundles.agda b/src/Function/Metric/Rational/Bundles.agda index 89067d2718..8bbc9f85d3 100644 --- a/src/Function/Metric/Rational/Bundles.agda +++ b/src/Function/Metric/Rational/Bundles.agda @@ -11,7 +11,7 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Data.Rational.Base hiding (_⊔_) -open import Function using (const) +open import Function.Base using (const) open import Level using (Level; suc; _⊔_) open import Relation.Binary.Core open import Relation.Binary.PropositionalEquality diff --git a/src/Function/Metric/Rational/Structures.agda b/src/Function/Metric/Rational/Structures.agda index 44339d296b..824f90b912 100644 --- a/src/Function/Metric/Rational/Structures.agda +++ b/src/Function/Metric/Rational/Structures.agda @@ -7,7 +7,7 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Data.Rational.Base -open import Function using (const) +open import Function.Base using (const) open import Level using (Level; suc) open import Relation.Binary hiding (Symmetric) open import Relation.Binary.PropositionalEquality using (_≡_) diff --git a/src/Function/Reasoning.agda b/src/Function/Reasoning.agda index 09747c0541..ea39d0b52e 100644 --- a/src/Function/Reasoning.agda +++ b/src/Function/Reasoning.agda @@ -19,4 +19,4 @@ infixl 0 ∋-syntax syntax ∋-syntax A a = a ∶ A -- Export pipeline functions -open import Function public using (_|>_; _|>′_) +open import Function.Base public using (_|>_; _|>′_) diff --git a/src/Reflection/AST/Meta.agda b/src/Reflection/AST/Meta.agda index 59ca4ae4db..93584f573c 100644 --- a/src/Reflection/AST/Meta.agda +++ b/src/Reflection/AST/Meta.agda @@ -8,8 +8,8 @@ module Reflection.AST.Meta where -import Data.Nat.Properties as ℕₚ using (_≟_) -open import Function using (_on_) +import Data.Nat.Properties as ℕₚ using (_≟_) +open import Function.Base using (_on_) open import Relation.Nullary.Decidable using (map′) open import Relation.Binary using (Rel; Decidable; DecidableEquality) import Relation.Binary.Construct.On as On diff --git a/src/Reflection/AST/Name.agda b/src/Reflection/AST/Name.agda index 203521330c..1baa63029f 100644 --- a/src/Reflection/AST/Name.agda +++ b/src/Reflection/AST/Name.agda @@ -8,10 +8,10 @@ module Reflection.AST.Name where -open import Data.List.Base using (List) -import Data.Product.Properties as Prodₚ using (≡-dec) -import Data.Word.Properties as Wₚ using (_≟_) -open import Function using (_on_) +open import Data.List.Base using (List) +import Data.Product.Properties as Prodₚ using (≡-dec) +import Data.Word.Properties as Wₚ using (_≟_) +open import Function.Base using (_on_) open import Relation.Nullary.Decidable using (map′) open import Relation.Binary using (Rel; Decidable; DecidableEquality) open import Relation.Binary.Construct.On using (decidable) diff --git a/src/Reflection/AST/Traversal.agda b/src/Reflection/AST/Traversal.agda index de28c8db2a..336935783e 100644 --- a/src/Reflection/AST/Traversal.agda +++ b/src/Reflection/AST/Traversal.agda @@ -11,12 +11,12 @@ open import Effect.Applicative using (RawApplicative) module Reflection.AST.Traversal {F : Set → Set} (AppF : RawApplicative F) where -open import Data.Nat using (ℕ; zero; suc; _+_) -open import Data.List using (List; []; _∷_; _++_; reverse; length) -open import Data.Product using (_×_; _,_) -open import Data.String using (String) -open import Function using (_∘_) -open import Reflection hiding (pure) +open import Data.Nat using (ℕ; zero; suc; _+_) +open import Data.List using (List; []; _∷_; _++_; reverse; length) +open import Data.Product using (_×_; _,_) +open import Data.String using (String) +open import Function.Base using (_∘_) +open import Reflection hiding (pure) open RawApplicative AppF diff --git a/src/Reflection/External.agda b/src/Reflection/External.agda index 3206ee2145..ba4e076426 100644 --- a/src/Reflection/External.agda +++ b/src/Reflection/External.agda @@ -16,7 +16,7 @@ open import Data.Product using (_×_; _,_) open import Data.String.Base as String using (String; _++_) open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]) open import Data.Unit.Base using (⊤; tt) -open import Function using (case_of_; _$_; _∘_) +open import Function.Base using (case_of_; _$_; _∘_) open import Reflection hiding (name) -- Type aliases for the various strings. diff --git a/src/Relation/Binary/OrderMorphism.agda b/src/Relation/Binary/OrderMorphism.agda index 9e2cb84ba3..fbf3781c78 100644 --- a/src/Relation/Binary/OrderMorphism.agda +++ b/src/Relation/Binary/OrderMorphism.agda @@ -16,7 +16,7 @@ Use Relation.Binary.Reasoning.Morphism instead." open import Relation.Binary open Poset -import Function as F +import Function.Base as F open import Level record _⇒-Poset_ {p₁ p₂ p₃ p₄ p₅ p₆} diff --git a/src/Relation/Unary/Algebra.agda b/src/Relation/Unary/Algebra.agda index f302cf7272..2d121be0fa 100644 --- a/src/Relation/Unary/Algebra.agda +++ b/src/Relation/Unary/Algebra.agda @@ -17,7 +17,7 @@ open import Data.Empty.Polymorphic using (⊥-elim) open import Data.Product as Product using (_,_; proj₁; proj₂; <_,_>; curry; uncurry) open import Data.Sum as Sum using (inj₁; inj₂; [_,_]) open import Data.Unit.Polymorphic using (tt) -open import Function using (id; const; _∘_) +open import Function.Base using (id; const; _∘_) open import Level open import Relation.Unary hiding (∅; U) open import Relation.Unary.Polymorphic using (∅; U) diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda index 5a545a4c77..25e21193be 100644 --- a/src/Tactic/Cong.agda +++ b/src/Tactic/Cong.agda @@ -24,7 +24,7 @@ module Tactic.Cong where -open import Function using (_$_) +open import Function.Base using (_$_) open import Data.Bool.Base using (true; false; if_then_else_; _∧_) open import Data.Char.Base as Char using (toℕ) diff --git a/src/Tactic/RingSolver/Core/AlmostCommutativeRing.agda b/src/Tactic/RingSolver/Core/AlmostCommutativeRing.agda index 84fe184f39..2817b21cf4 100644 --- a/src/Tactic/RingSolver/Core/AlmostCommutativeRing.agda +++ b/src/Tactic/RingSolver/Core/AlmostCommutativeRing.agda @@ -15,7 +15,7 @@ open import Algebra.Structures using (IsCommutativeSemiring) open import Algebra.Definitions open import Algebra.Bundles using (RawRing; CommutativeRing; CommutativeSemiring) import Algebra.Morphism as Morphism -open import Function hiding (Morphism) +open import Function.Base using (id) open import Level open import Data.Maybe.Base as Maybe using (Maybe; just; nothing) diff --git a/tests/data/appending/Main.agda b/tests/data/appending/Main.agda index 93ece5eda0..b5fc0a48a6 100644 --- a/tests/data/appending/Main.agda +++ b/tests/data/appending/Main.agda @@ -7,7 +7,7 @@ open import Data.List using (replicate) open import Data.String using (toList; fromList) open import IO -open import Function using (_$_) +open import Function.Base using (_$_) open import TakeWhile diff --git a/tests/data/colist/Main.agda b/tests/data/colist/Main.agda index a50b5b85fe..d47585dd6e 100644 --- a/tests/data/colist/Main.agda +++ b/tests/data/colist/Main.agda @@ -11,7 +11,7 @@ import Data.Fin.Show as Fin open import Data.String.Base using (String; _++_; parens) open import Data.Unit.Polymorphic.Base using (⊤) open import Codata.Sized.Thunk -open import Function using (_$_; _∘_; id) +open import Function.Base using (_$_; _∘_; id) open import Relation.Nullary open import Codata.Musical.Notation