Refine imports in Reflection.AST (#2072)

Author: Saransh-cpp

src/Reflection/AST/Abstraction.agda

@@ -11,8 +11,8 @@ module Reflection.AST.Abstraction where
 open import Data.String.Base as String                 using (String)
 open import Data.String.Properties as String           using (_≟_)
 open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
-open import Level
-open import Relation.Nullary.Decidable                 using (Dec; map′; _×-dec_)
+open import Level using (Level)
+open import Relation.Nullary.Decidable.Core            using (Dec; map′; _×-dec_)
 open import Relation.Binary.Definitions                using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
 

src/Reflection/AST/AlphaEquality.agda

@@ -8,12 +8,12 @@
 
 module Reflection.AST.AlphaEquality where
 
-open import Data.Bool.Base                using (Bool; true; false; _∧_)
-open import Data.List.Base                using ([]; _∷_)
-open import Data.Nat.Base as ℕ            using (ℕ; zero; suc; _≡ᵇ_)
-open import Data.Product.Base             using (_,_)
-open import Relation.Nullary.Decidable    using (⌊_⌋)
-open import Relation.Binary.Definitions   using (DecidableEquality)
+open import Data.Bool.Base                   using (Bool; true; false; _∧_)
+open import Data.List.Base                   using ([]; _∷_)
+open import Data.Nat.Base as ℕ               using (ℕ; zero; suc; _≡ᵇ_)
+open import Data.Product.Base                using (_,_)
+open import Relation.Nullary.Decidable.Core  using (⌊_⌋)
+open import Relation.Binary.Definitions      using (DecidableEquality)
 
 open import Reflection.AST.Abstraction
 open import Reflection.AST.Argument

src/Reflection/AST/Argument.agda

@@ -10,7 +10,7 @@ module Reflection.AST.Argument where
 
 open import Data.List.Base as List                     using (List; []; _∷_)
 open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
-open import Relation.Nullary.Decidable                 using (Dec; map′; _×-dec_)
+open import Relation.Nullary.Decidable.Core            using (Dec; map′; _×-dec_)
 open import Relation.Binary.Definitions                using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
 open import Level

src/Reflection/AST/Argument/Information.agda

@@ -9,7 +9,7 @@
 module Reflection.AST.Argument.Information where
 
 open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
-open import Relation.Nullary.Decidable                 using (map′; _×-dec_)
+open import Relation.Nullary.Decidable.Core            using (map′; _×-dec_)
 open import Relation.Binary.Definitions                using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
 

src/Reflection/AST/Argument/Modality.agda

@@ -9,7 +9,7 @@
 module Reflection.AST.Argument.Modality where
 
 open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
-open import Relation.Nullary.Decidable                 using (map′; _×-dec_)
+open import Relation.Nullary.Decidable.Core            using (map′; _×-dec_)
 open import Relation.Binary.Definitions                using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
 

src/Reflection/AST/Argument/Quantity.agda

@@ -8,7 +8,7 @@
 
 module Reflection.AST.Argument.Quantity where
 
-open import Relation.Nullary                           using (yes; no)
+open import Relation.Nullary.Decidable.Core           using (yes; no)
 open import Relation.Binary.Definitions                using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (refl)
 

src/Reflection/AST/Argument/Relevance.agda

@@ -8,7 +8,7 @@
 
 module Reflection.AST.Argument.Relevance where
 
-open import Relation.Nullary                           using (yes; no)
+open import Relation.Nullary.Decidable.Core            using (yes; no)
 open import Relation.Binary.Definitions                using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (refl)
 

src/Reflection/AST/Argument/Visibility.agda

@@ -8,7 +8,7 @@
 
 module Reflection.AST.Argument.Visibility where
 
-open import Relation.Nullary                           using (yes; no)
+open import Relation.Nullary.Decidable.Core            using (yes; no)
 open import Relation.Binary.Definitions                using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (refl)
 

src/Reflection/AST/Definition.agda

@@ -11,7 +11,7 @@ module Reflection.AST.Definition where
 import Data.List.Properties as Listₚ                   using (≡-dec)
 import Data.Nat.Properties as ℕₚ                       using (_≟_)
 open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
-open import Relation.Nullary.Decidable                 using (map′; _×-dec_; yes; no)
+open import Relation.Nullary.Decidable.Core            using (map′; _×-dec_; yes; no)
 open import Relation.Binary.Definitions                using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)
 

src/Reflection/AST/Literal.agda

@@ -8,16 +8,15 @@
 
 module Reflection.AST.Literal where
 
-open import Data.Bool.Base   using (Bool; true; false)
-import Data.Char as Char     using (_≟_)
-import Data.Float as Float   using (_≟_)
-import Data.Nat as ℕ        using (_≟_)
-import Data.String.Properties as String using (_≟_)
-import Data.Word as Word     using (_≟_)
+open import Data.Bool.Base using (Bool; true; false)
+import Data.Char.Properties as Char
+import Data.Float.Properties as Float
+import Data.Nat.Properties as ℕ
+import Data.String.Properties as String
+import Data.Word.Properties as Word
 import Reflection.AST.Meta as Meta
 import Reflection.AST.Name as Name
-open import Relation.Nullary                           using (yes; no)
-open import Relation.Nullary.Decidable                 using (map′; isYes)
+open import Relation.Nullary.Decidable.Core            using (yes; no; map′; isYes)
 open import Relation.Binary.Definitions                using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 

src/Reflection/AST/Meta.agda

@@ -8,9 +8,9 @@
 
 module Reflection.AST.Meta where
 
-import Data.Nat.Properties as ℕₚ                       using (_≟_)
+import Data.Nat.Properties as ℕₚ
 open import Function.Base                              using (_on_)
-open import Relation.Nullary.Decidable                 using (map′)
+open import Relation.Nullary.Decidable.Core            using (map′)
 open import Relation.Binary.Core                       using (Rel)
 open import Relation.Binary.Definitions                using (Decidable; DecidableEquality)
 import Relation.Binary.Construct.On as On

src/Reflection/AST/Name.agda

@@ -12,7 +12,7 @@ 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.Nullary.Decidable.Core            using (map′)
 open import Relation.Binary.Core                       using (Rel)
 open import Relation.Binary.Definitions                using (Decidable; DecidableEquality)
 open import Relation.Binary.Construct.On               using (decidable)

src/Reflection/AST/Show.agda

@@ -11,16 +11,16 @@
 
 module Reflection.AST.Show where
 
-import Data.Char as Char   using (show)
-import Data.Float as Float using (show)
+import Data.Char.Base as Char
+import Data.Float.Base as Float
 open import Data.List.Base hiding (_++_; intersperse)
-import Data.Nat.Show as ℕ using (show)
+import Data.Nat.Show as ℕ
 open import Data.String.Base as String using (String; _++_; intersperse; braces; parens; _<+>_)
 open import Data.String as String using (parensIfSpace)
 open import Data.Product.Base using (_×_; _,_)
-import Data.Word as Word   using (toℕ)
+import Data.Word.Base as Word
 open import Function.Base using (id; _∘′_; case_of_)
-open import Relation.Nullary.Decidable using (yes; no)
+open import Relation.Nullary.Decidable.Core using (yes; no)
 
 open import Reflection.AST.Abstraction hiding (map)
 open import Reflection.AST.Argument hiding (map)

src/Reflection/AST/Term.agda

@@ -10,7 +10,8 @@ module Reflection.AST.Term where
 
 open import Data.List.Base as List                     hiding (_++_)
 open import Data.List.Properties                       using (∷-dec)
-open import Data.Nat as ℕ                              using (ℕ; zero; suc)
+open import Data.Nat.Base                              using (ℕ; zero; suc)
+import Data.Nat.Properties as ℕ
 open import Data.Product.Base                          using (_×_; _,_; <_,_>; uncurry; map₁)
 open import Data.Product.Properties                    using (,-injective)
 open import Data.Maybe.Base                            using (Maybe; just; nothing)

src/Reflection/AST/Traversal.agda

@@ -11,7 +11,7 @@ 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.Nat.Base     using (ℕ; zero; suc; _+_)
 open import Data.List.Base    using (List; []; _∷_; _++_; reverse; length)
 open import Data.String.Base  using (String)
 open import Data.Product.Base using (_×_; _,_)