Skip to content

Commit 9a240ee

Browse files
authored
More Data.Product simplifications (#2039)
1 parent bfa4f8b commit 9a240ee

File tree

83 files changed

+83
-83
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

83 files changed

+83
-83
lines changed

README/Data/Nat/Induction.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ module README.Data.Nat.Induction where
99

1010
open import Data.Nat
1111
open import Data.Nat.Induction
12-
open import Data.Product using (_,_)
12+
open import Data.Product.Base using (_,_)
1313
open import Function.Base using (_∘_)
1414
open import Induction.WellFounded
1515
open import Relation.Binary.PropositionalEquality

README/Data/Tree/AVL.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ import Data.Tree.AVL
2020
-- natural numbers as keys and vectors of strings as values.
2121

2222
open import Data.Nat.Properties using (<-strictTotalOrder)
23-
open import Data.Product as Prod using (_,_; _,′_)
23+
open import Data.Product.Base as Prod using (_,_; _,′_)
2424
open import Data.String.Base using (String)
2525
open import Data.Vec.Base using (Vec; _∷_; [])
2626
open import Relation.Binary.PropositionalEquality

README/Function/Reasoning.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ open import Data.String.Base as String using (String; toList; fromList)
3939
open import Data.String.Properties as String using (_==_)
4040
open import Function.Base using (_∘_)
4141
open import Data.Bool hiding (_≤?_)
42-
open import Data.Product as P using (_×_; <_,_>; uncurry; proj₁)
42+
open import Data.Product.Base as P using (_×_; <_,_>; uncurry; proj₁)
4343
open import Agda.Builtin.Equality
4444

4545
-- This can give us for instance this decomposition of a function

README/Nary.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ open import Data.Nat.Properties
1515
open import Data.Fin using (Fin; fromℕ; #_; inject₁)
1616
open import Data.List
1717
open import Data.List.Properties
18-
open import Data.Product using (_×_; _,_)
18+
open import Data.Product.Base using (_×_; _,_)
1919
open import Data.Sum.Base using (inj₁; inj₂)
2020
open import Function.Base using (id; flip; _∘′_)
2121
open import Relation.Nullary

src/Algebra/Lattice/Construct/Subst/Equality.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@
1212
open import Algebra.Core using (Op₂)
1313
open import Algebra.Definitions
1414
open import Algebra.Lattice.Structures
15-
open import Data.Product as Prod
15+
open import Data.Product.Base as Prod
1616
open import Function.Base
1717
open import Relation.Binary.Core
1818

src/Codata/Guarded/M.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ module Codata.Guarded.M where
1111
open import Level
1212
open import Data.Container.Core hiding (map; Shape; Position)
1313
open import Function.Base
14-
open import Data.Product hiding (map)
14+
open import Data.Product.Base hiding (map)
1515

1616
-- The family of M-types
1717

src/Codata/Guarded/Stream.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ open import Level hiding (suc)
1212
open import Data.Nat.Base
1313
open import Function.Base
1414
open import Data.List.Base as List using (List; []; _∷_)
15-
open import Data.Product hiding (map)
15+
open import Data.Product.Base hiding (map)
1616
open import Data.Vec.Base using (Vec; []; _∷_)
1717
open import Data.List.NonEmpty.Base as List⁺ using (List⁺; _∷_)
1818
open import Algebra.Core

src/Codata/Musical/M.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ module Codata.Musical.M where
1010

1111
open import Codata.Musical.Notation
1212
open import Level
13-
open import Data.Product hiding (map)
13+
open import Data.Product.Base hiding (map)
1414
open import Data.Container.Core as C hiding (map)
1515

1616
-- The family of M-types.

src/Codata/Sized/Delay.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ open import Data.Empty
1616
open import Relation.Nullary
1717
open import Data.Nat.Base
1818
open import Data.Maybe.Base hiding (map ; fromMaybe ; zipWith ; alignWith ; zip ; align)
19-
open import Data.Product as P hiding (map ; zip)
19+
open import Data.Product.Base as P hiding (map ; zip)
2020
open import Data.Sum.Base as S hiding (map)
2121
open import Data.These.Base as T using (These; this; that; these)
2222
open import Function.Base using (id)

src/Codata/Sized/M.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ module Codata.Sized.M where
1111
open import Size
1212
open import Level
1313
open import Codata.Sized.Thunk using (Thunk; force)
14-
open import Data.Product hiding (map)
14+
open import Data.Product.Base hiding (map)
1515
open import Data.Container.Core as C hiding (map)
1616

1717
data M {s p} (C : Container s p) (i : Size) : Set (s ⊔ p) where

0 commit comments

Comments
 (0)