Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Refine imports in Reflection.AST #2072

Merged
merged 2 commits into from
Sep 12, 2023
Merged

Refine imports in Reflection.AST #2072

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
281eaf6
Refine imports in `Reflection.AST`
Saransh-cpp Aug 23, 2023
1f7107a
Spaces
Saransh-cpp Aug 23, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions src/Reflection/AST/Abstraction.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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₂)

Expand Down
12 changes: 6 additions & 6 deletions src/Reflection/AST/AlphaEquality.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/Reflection/AST/Argument.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/Reflection/AST/Argument/Information.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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₂)

Expand Down
2 changes: 1 addition & 1 deletion src/Reflection/AST/Argument/Modality.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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₂)

Expand Down
2 changes: 1 addition & 1 deletion src/Reflection/AST/Argument/Quantity.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
2 changes: 1 addition & 1 deletion src/Reflection/AST/Argument/Relevance.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
2 changes: 1 addition & 1 deletion src/Reflection/AST/Argument/Visibility.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
2 changes: 1 addition & 1 deletion src/Reflection/AST/Definition.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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₂)

Expand Down
15 changes: 7 additions & 8 deletions src/Reflection/AST/Literal.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
4 changes: 2 additions & 2 deletions src/Reflection/AST/Meta.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/Reflection/AST/Name.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
10 changes: 5 additions & 5 deletions src/Reflection/AST/Show.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
3 changes: 2 additions & 1 deletion src/Reflection/AST/Term.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion src/Reflection/AST/Traversal.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 (_×_; _,_)
Expand Down