Skip to content

Tighten imports #2334

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

Merged
merged 5 commits into from
Apr 4, 2024
Merged

Tighten imports #2334

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
e79c190
tighten imports in some files, and make imports explicit in others. D…
JacquesCarette Mar 29, 2024
2bba1e5
more tightening of imports
JacquesCarette Mar 29, 2024
c8cbf7f
and even more tightening of imports
JacquesCarette Mar 29, 2024
50e0873
some explicit for precision
JacquesCarette Mar 29, 2024
0fa3713
Merge branch 'master' into TightenImports
gallais Apr 3, 2024
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/Algebra/Definitions/RawMagma.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,10 +10,10 @@

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

open import Algebra.Bundles using (RawMagma)
open import Algebra.Bundles.Raw using (RawMagma)
open import Data.Product.Base using (_×_; ∃)
open import Level using (_⊔_)
open import Relation.Binary.Core
open import Relation.Binary.Core using (Rel)
open import Relation.Nullary.Negation using (¬_)

module Algebra.Definitions.RawMagma
Expand Down
6 changes: 3 additions & 3 deletions src/Data/Maybe/Base.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,9 +15,9 @@ open import Data.Bool.Base using (Bool; true; false; not)
open import Data.Unit.Base using (⊤)
open import Data.These.Base using (These; this; that; these)
open import Data.Product.Base as Prod using (_×_; _,_)
open import Function.Base
open import Relation.Nullary.Reflects
open import Relation.Nullary.Decidable.Core
open import Function.Base using (const; _∘_; id)
open import Relation.Nullary.Reflects using (invert)
open import Relation.Nullary.Decidable.Core using (Dec; _because_)

private
variable
Expand Down
5 changes: 3 additions & 2 deletions src/Data/Product/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,13 +8,14 @@

module Data.Product.Properties where

open import Axiom.UniquenessOfIdentityProofs
open import Data.Product.Base
open import Axiom.UniquenessOfIdentityProofs using (UIP; module Decidable⇒UIP)
open import Data.Product.Base using (_,_; Σ; _×_; map; swap; ∃; ∃₂)
open import Function.Base using (_∋_; _∘_; id)
open import Function.Bundles using (_↔_; mk↔ₛ′)
open import Level using (Level)
open import Relation.Binary.Definitions using (DecidableEquality)
open import Relation.Binary.PropositionalEquality
using (_≡_; _≗_; subst; cong; cong₂; cong′; refl)
open import Relation.Nullary.Decidable as Dec using (Dec; yes; no)

private
Expand Down
2 changes: 1 addition & 1 deletion src/Function/Indexed/Relation/Binary/Equality.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@

module Function.Indexed.Relation.Binary.Equality where

open import Relation.Binary using (Setoid)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Indexed.Heterogeneous using (IndexedSetoid)

-- A variant of setoid which uses the propositional equality setoid
Expand Down