Cut down Function imports (#2006)

Saransh-cpp · MatthewDaggitt · commit b093306b6bf9 · 2023-10-13T11:34:27.000+09:00
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
diff --git a/src/Reflection/External.agda b/src/Reflection/External.agda
diff --git a/src/Relation/Binary/OrderMorphism.agda b/src/Relation/Binary/OrderMorphism.agda
diff --git a/src/Relation/Unary/Algebra.agda b/src/Relation/Unary/Algebra.agda
diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda
diff --git a/src/Tactic/RingSolver/Core/AlmostCommutativeRing.agda b/src/Tactic/RingSolver/Core/AlmostCommutativeRing.agda
diff --git a/tests/data/appending/Main.agda b/tests/data/appending/Main.agda
diff --git a/tests/data/colist/Main.agda b/tests/data/colist/Main.agda
