Skip to content

Commit 4f591ae

Browse files
Sofia-InsaMatthewDaggitt
authored andcommitted
Simplify import of Data.List.Relation.Binary.Pointwise in agda-stdl (#2019)
* Simplify import of `Data.List.Relation.Binary.Pointwise` in agda-stdl * rectifications on Data.List.Relation.Binary.Pointwise import * rectifications on Data.List.Relation.Binary.Pointwise import * Delete weights-README.dot * Delete weight.png * Delete README.dot
1 parent 6112ef1 commit 4f591ae

File tree

22 files changed

+27
-25
lines changed

22 files changed

+27
-25
lines changed

README/Case.agda

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,6 @@ open import Data.Product
1616
open import Function.Base using (case_of_; case_return_of_)
1717
open import Relation.Nullary
1818
open import Relation.Binary
19-
open import Relation.Binary.PropositionalEquality
2019

2120
------------------------------------------------------------------------
2221
-- Different types of pattern-matching lambdas

README/Data/List/Relation/Binary/Equality.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,7 @@ open import Relation.Binary.PropositionalEquality using (_≗_)
5454
-- to `_≗_`. However instead of using the pointwise module directly
5555
-- to write:
5656

57-
open import Data.List.Relation.Binary.Pointwise using (Pointwise)
57+
open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise)
5858

5959
lem₃ : Pointwise _≗_ ((λ x x + 1) ∷ []) ((λ x x + 21) ∷ [])
6060
lem₃ = {!!}

README/Inspect.agda

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,8 @@ module README.Inspect where
1515
open import Data.Nat.Base
1616
open import Data.Nat.Properties
1717
open import Data.Product
18-
open import Relation.Binary.PropositionalEquality
18+
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
19+
open import Relation.Binary.PropositionalEquality using (inspect)
1920

2021
------------------------------------------------------------------------
2122
-- Using inspect

src/Codata/Sized/Colist/Bisimilarity.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ open import Size
1313
open import Codata.Sized.Thunk
1414
open import Codata.Sized.Colist
1515
open import Data.List.Base using (List; []; _∷_)
16-
open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
16+
open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_)
1717
open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_)
1818
open import Relation.Binary
1919
open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_)

src/Codata/Sized/Stream/Bisimilarity.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ open import Codata.Sized.Thunk
1313
open import Codata.Sized.Stream
1414
open import Level
1515
open import Data.List.NonEmpty as List⁺ using (_∷_)
16-
open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
16+
open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_)
1717
open import Relation.Binary
1818
open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_)
1919
import Relation.Binary.PropositionalEquality.Properties as Eq

src/Data/Container/Indexed/FreeMonad.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ open import Data.Product
1919
open import Data.W.Indexed
2020
open import Relation.Unary
2121
open import Relation.Unary.PredicateTransformer
22-
open import Relation.Binary.PropositionalEquality
22+
open import Relation.Binary.PropositionalEquality.Core using (refl)
2323

2424
------------------------------------------------------------------------
2525

src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,7 @@ open import Relation.Nullary.Negation using (¬_; contradiction)
2222
open import Relation.Unary as U using (Pred)
2323
open import Relation.Binary using (REL; _⇒_; Decidable; Trans; Antisym)
2424
open import Relation.Binary.PropositionalEquality.Core using (_≢_; refl; cong)
25-
26-
open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise)
25+
open import Data.List.Relation.Binary.Pointwise.Base as Pointwise using (Pointwise)
2726
open import Data.List.Relation.Binary.Infix.Heterogeneous
2827
open import Data.List.Relation.Binary.Prefix.Heterogeneous
2928
as Prefix using (Prefix; []; _∷_)

src/Data/List/Relation/Binary/Lex/NonStrict.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ open import Function.Base
1616
open import Data.Unit.Base using (⊤; tt)
1717
open import Data.Product
1818
open import Data.List.Base
19-
open import Data.List.Relation.Binary.Pointwise using (Pointwise; [])
19+
open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; [])
2020
import Data.List.Relation.Binary.Lex.Strict as Strict
2121
open import Level
2222
open import Relation.Nullary

src/Data/List/Relation/Binary/Permutation/Homogeneous.agda

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,10 @@
99
module Data.List.Relation.Binary.Permutation.Homogeneous where
1010

1111
open import Data.List.Base using (List; _∷_)
12-
open import Data.List.Relation.Binary.Pointwise as Pointwise
12+
open import Data.List.Relation.Binary.Pointwise.Base as Pointwise
1313
using (Pointwise)
14+
open import Data.List.Relation.Binary.Pointwise.Properties as Pointwise
15+
using (symmetric)
1416
open import Level using (Level; _⊔_)
1517
open import Relation.Binary
1618

src/Data/List/Relation/Binary/Permutation/Setoid.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ module Data.List.Relation.Binary.Permutation.Setoid
1313

1414
open import Data.List.Base using (List; _∷_)
1515
import Data.List.Relation.Binary.Permutation.Homogeneous as Homogeneous
16-
import Data.List.Relation.Binary.Pointwise as Pointwise
16+
import Data.List.Relation.Binary.Pointwise.Properties as Pointwise using (refl)
1717
open import Data.List.Relation.Binary.Equality.Setoid S
1818
open import Data.Nat.Base using (ℕ; zero; suc; _+_)
1919
open import Level using (_⊔_)

0 commit comments

Comments
 (0)