Skip to content

Commit 7c82a8e

Browse files
Saransh-cppSaransh-cpp
authored
Final Relation.Binary simplifications (#2068)
1 parent f77a02a commit 7c82a8e

File tree

161 files changed

+513
-169
lines changed

Some content is hidden

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

161 files changed

+513
-169
lines changed

‎src/Codata/Sized/Conat/Properties.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ open import Codata.Sized.Conat.Bisimilarity
1616
open import Function.Base using (_∋_)
1717
open import Relation.Nullary
1818
open import Relation.Nullary.Decidable using (map′)
19-
open import Relation.Binary
19+
open import Relation.Binary.Definitions using (Decidable)
2020

2121
private
2222
variable

‎src/Data/AVL/Indexed/WithK.agda

+2-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,8 @@
66

77
{-# OPTIONS --with-K --safe #-}
88

9-
open import Relation.Binary
9+
open import Relation.Binary.Core using (Rel)
10+
open import Relation.Binary.Structures using (IsStrictTotalOrder)
1011
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; subst)
1112

1213
module Data.AVL.Indexed.WithK

‎src/Data/AVL/IndexedMap.agda

+2-1
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,8 @@
77
{-# OPTIONS --cubical-compatible --safe #-}
88

99
open import Data.Product.Base using (∃)
10-
open import Relation.Binary
10+
open import Relation.Binary.Core using (Rel)
11+
open import Relation.Binary.Structures using (IsStrictTotalOrder)
1112
open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong; subst)
1213
import Data.Tree.AVL.Value
1314

‎src/Data/AVL/Key.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66

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

9-
open import Relation.Binary
9+
open import Relation.Binary.Bundles using (StrictTotalOrder)
1010

1111
module Data.AVL.Key
1212
{a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)

‎src/Data/Bool.agda

-1
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@
99
module Data.Bool where
1010

1111
open import Relation.Nullary
12-
open import Relation.Binary
1312
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
1413

1514
------------------------------------------------------------------------

‎src/Data/Char/Properties.agda

+7-1
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,13 @@ open import Data.Product.Base using (_,_)
1717
open import Function.Base
1818
open import Relation.Nullary using (¬_; yes; no)
1919
open import Relation.Nullary.Decidable using (map′; isYes)
20-
open import Relation.Binary
20+
open import Relation.Binary.Core using (_⇒_)
21+
open import Relation.Binary.Bundles
22+
using (Setoid; DecSetoid; StrictPartialOrder; StrictTotalOrder; Preorder; Poset; DecPoset)
23+
open import Relation.Binary.Structures
24+
using (IsDecEquivalence; IsStrictPartialOrder; IsStrictTotalOrder; IsPreorder; IsPartialOrder; IsDecPartialOrder; IsEquivalence)
25+
open import Relation.Binary.Definitions
26+
using (Decidable; Trichotomous; Irreflexive; Transitive; Asymmetric; Antisymmetric; Symmetric; Substitutive; Reflexive; tri<; tri≈; tri>)
2127
import Relation.Binary.Construct.On as On
2228
import Relation.Binary.Construct.Subst.Equality as Subst
2329
import Relation.Binary.Construct.Closure.Reflexive as Refl

‎src/Data/Container/Properties.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@
99
module Data.Container.Properties where
1010

1111
import Function.Base as F
12-
open import Relation.Binary
12+
open import Relation.Binary.Bundles using (Setoid)
1313

1414
open import Data.Container.Core
1515
open import Data.Container.Relation.Binary.Equality.Setoid

‎src/Data/Container/Related.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ module Data.Container.Related where
1212
open import Level using (_⊔_)
1313
open import Data.Container.Core
1414
import Function.Related as Related
15-
open import Relation.Binary
15+
open import Relation.Binary.Bundles using (Preorder; Setoid)
1616
open import Data.Container.Membership
1717

1818
open Related public

‎src/Data/Container/Relation/Binary/Equality/Setoid.agda

+4-1
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,10 @@ open import Relation.Binary.Bundles using (Setoid)
1111
module Data.Container.Relation.Binary.Equality.Setoid {c e} (S : Setoid c e) where
1212

1313
open import Level using (_⊔_; suc)
14-
open import Relation.Binary
14+
open import Relation.Binary.Core using (Rel)
15+
open import Relation.Binary.Structures using (IsEquivalence)
16+
open import Relation.Binary.Definitions
17+
using (Reflexive; Symmetric; Transitive)
1518

1619
open import Data.Container.Core
1720
open import Data.Container.Relation.Binary.Pointwise

‎src/Data/Container/Relation/Binary/Pointwise/Properties.agda

+4-1
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,10 @@ open import Data.Container.Core
1313
open import Data.Container.Relation.Binary.Pointwise
1414
open import Data.Product.Base using (_,_; Σ-syntax; -,_)
1515
open import Level using (_⊔_)
16-
open import Relation.Binary
16+
open import Relation.Binary.Core using (Rel)
17+
open import Relation.Binary.Definitions
18+
using (Reflexive; Symmetric; Transitive)
19+
open import Relation.Binary.Core using (Rel)
1720
open import Relation.Binary.PropositionalEquality.Core as P
1821
using (_≡_; subst; cong)
1922

‎src/Data/Fin/Induction.agda

+4-2
Original file line numberDiff line numberDiff line change
@@ -21,8 +21,10 @@ open import Function.Base using (flip; _$_)
2121
open import Induction
2222
open import Induction.WellFounded as WF
2323
open import Level using (Level)
24-
open import Relation.Binary
25-
using (Rel; Decidable; IsPartialOrder; IsStrictPartialOrder; StrictPartialOrder)
24+
open import Relation.Binary.Core using (Rel)
25+
open import Relation.Binary.Bundles using (StrictPartialOrder)
26+
open import Relation.Binary.Structures using (IsPartialOrder; IsStrictPartialOrder)
27+
open import Relation.Binary.Definitions using (Decidable)
2628
import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd
2729
import Relation.Binary.Construct.Flip.Ord as Ord
2830
import Relation.Binary.Construct.NonStrictToStrict as ToStrict

‎src/Data/Float/Properties.agda

+6-1
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,12 @@ import Data.Word.Base as Word
1717
import Data.Word.Properties as Wₚ
1818
open import Function.Base using (_∘_)
1919
open import Relation.Nullary.Decidable as RN using (map′)
20-
open import Relation.Binary
20+
open import Relation.Binary.Core using (_⇒_)
21+
open import Relation.Binary.Bundles using (Setoid; DecSetoid)
22+
open import Relation.Binary.Structures
23+
using (IsEquivalence; IsDecEquivalence)
24+
open import Relation.Binary.Definitions
25+
using (Reflexive; Symmetric; Transitive; Substitutive; Decidable; DecidableEquality)
2126
import Relation.Binary.Construct.On as On
2227
open import Relation.Binary.PropositionalEquality
2328

‎src/Data/Integer/Divisibility.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ import Data.Nat.Properties as ℕᵖ
1818
import Data.Nat.Divisibility as ℕᵈ
1919
import Data.Nat.Coprimality as ℕᶜ
2020
open import Level
21-
open import Relation.Binary
21+
open import Relation.Binary.Core using (Rel; _Preserves_⟶_)
2222
open import Relation.Binary.PropositionalEquality
2323

2424
------------------------------------------------------------------------

‎src/Data/Integer/Divisibility/Signed.agda

+5-1
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,11 @@ import Data.Nat.Properties as ℕ
2121
import Data.Sign as S
2222
import Data.Sign.Properties as SProp
2323
open import Level
24-
open import Relation.Binary
24+
open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_)
25+
open import Relation.Binary.Bundles using (Preorder)
26+
open import Relation.Binary.Structures using (IsPreorder)
27+
open import Relation.Binary.Definitions
28+
using (Reflexive; Transitive; Decidable)
2529
open import Relation.Binary.PropositionalEquality
2630
import Relation.Binary.Reasoning.Preorder as PreorderReasoning
2731
open import Relation.Nullary.Decidable using (yes; no)

‎src/Data/Integer/Properties.agda

+7-1
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,13 @@ open import Data.Sign as Sign using (Sign) renaming (_*_ to _𝕊*_)
2727
import Data.Sign.Properties as 𝕊ₚ
2828
open import Function.Base using (_∘_; _$_; id)
2929
open import Level using (0ℓ)
30-
open import Relation.Binary
30+
open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
31+
open import Relation.Binary.Bundles using
32+
(Setoid; DecSetoid; Preorder; TotalPreorder; Poset; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder)
33+
open import Relation.Binary.Structures
34+
using (IsPreorder; IsTotalPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder)
35+
open import Relation.Binary.Definitions
36+
using (DecidableEquality; Reflexive; Transitive; Antisymmetric; Total; Decidable; Irrelevant; Irreflexive; Asymmetric; Trans; Trichotomous; tri≈; tri<; tri>)
3137
open import Relation.Binary.PropositionalEquality
3238
open import Relation.Nullary using (yes; no; ¬_)
3339
import Relation.Nullary.Reflects as Reflects

‎src/Data/List/Countdown.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88
{-# OPTIONS --cubical-compatible --safe #-}
99

1010
open import Level using (0ℓ)
11-
open import Relation.Binary
11+
open import Relation.Binary.Bundles using (DecSetoid)
1212

1313
module Data.List.Countdown (D : DecSetoid 0ℓ 0ℓ) where
1414

‎src/Data/List/Fresh/Membership/Setoid.agda

+2-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,8 @@
66

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

9-
open import Relation.Binary
9+
open import Relation.Binary.Core using (Rel)
10+
open import Relation.Binary.Bundles using (Setoid)
1011

1112
module Data.List.Fresh.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where
1213

‎src/Data/List/Membership/Setoid.agda

+2-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,8 @@
66

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

9-
open import Relation.Binary
9+
open import Relation.Binary.Bundles using (Setoid)
10+
open import Relation.Binary.Definitions using (_Respects_)
1011

1112
module Data.List.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where
1213

‎src/Data/List/Relation/Binary/BagAndSetEquality.agda

+2-1
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,8 @@ open import Function.Inverse as Inv using (_↔_; Inverse; inverse)
3636
open import Function.Related as Related
3737
using (↔⇒; ⌊_⌋; ⌊_⌋→; ⇒→; K-refl; SK-sym)
3838
open import Function.Related.TypeIsomorphisms
39-
open import Relation.Binary
39+
open import Relation.Binary.Core using (_⇒_)
40+
open import Relation.Binary.Bundles using (Preorder; Setoid)
4041
import Relation.Binary.Reasoning.Setoid as EqR
4142
import Relation.Binary.Reasoning.Preorder as PreorderReasoning
4243
open import Relation.Binary.PropositionalEquality as P

‎src/Data/List/Relation/Binary/Disjoint/Propositional.agda

-2
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,6 @@
66

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

9-
open import Relation.Binary
10-
119
module Data.List.Relation.Binary.Disjoint.Propositional
1210
{a} {A : Set a} where
1311

‎src/Data/List/Relation/Binary/Disjoint/Setoid.agda

+2-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,8 @@
66

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

9-
open import Relation.Binary
9+
open import Relation.Binary.Core using (Rel)
10+
open import Relation.Binary.Bundles using (Setoid)
1011

1112
module Data.List.Relation.Binary.Disjoint.Setoid {c ℓ} (S : Setoid c ℓ) where
1213

‎src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda

+2-1
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,8 @@ open import Data.List.Relation.Unary.All.Properties using (¬Any⇒All¬)
1616
open import Data.List.Relation.Unary.Any.Properties using (++⁻)
1717
open import Data.Product.Base using (_,_)
1818
open import Data.Sum.Base using (inj₁; inj₂)
19-
open import Relation.Binary
19+
open import Relation.Binary.Bundles using (Setoid)
20+
open import Relation.Binary.Definitions using (Symmetric)
2021
open import Relation.Nullary.Negation using (¬_)
2122

2223
------------------------------------------------------------------------

‎src/Data/List/Relation/Binary/Equality/DecPropositional.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@
1010

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

13-
open import Relation.Binary
13+
open import Relation.Binary.Definitions using (Decidable)
1414
open import Relation.Binary.PropositionalEquality
1515

1616
module Data.List.Relation.Binary.Equality.DecPropositional

‎src/Data/List/Relation/Binary/Equality/DecSetoid.agda

+3-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,9 @@
66

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

9-
open import Relation.Binary
9+
open import Relation.Binary.Bundles using (DecSetoid)
10+
open import Relation.Binary.Structures using (IsDecEquivalence)
11+
open import Relation.Binary.Definitions using (Decidable)
1012

1113
module Data.List.Relation.Binary.Equality.DecSetoid
1214
{a ℓ} (DS : DecSetoid a ℓ) where

‎src/Data/List/Relation/Binary/Equality/Propositional.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@
1010

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

13-
open import Relation.Binary
13+
open import Relation.Binary.Core using (_⇒_)
1414

1515
module Data.List.Relation.Binary.Equality.Propositional {a} {A : Set a} where
1616

‎src/Data/List/Relation/Binary/Infix/Homogeneous/Properties.agda

+3-1
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,9 @@ module Data.List.Relation.Binary.Infix.Homogeneous.Properties where
1010

1111
open import Level
1212
open import Function.Base using (_∘′_)
13-
open import Relation.Binary
13+
open import Relation.Binary.Core using (REL)
14+
open import Relation.Binary.Structures
15+
using (IsPreorder; IsPartialOrder; IsDecPartialOrder)
1416

1517
open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise)
1618
open import Data.List.Relation.Binary.Infix.Heterogeneous

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

+7-1
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,13 @@ open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; [])
1919
import Data.List.Relation.Binary.Lex.Strict as Strict
2020
open import Level
2121
open import Relation.Nullary
22-
open import Relation.Binary
22+
open import Relation.Binary.Core using (Rel; _⇒_)
23+
open import Relation.Binary.Bundles
24+
using (Poset; StrictPartialOrder; DecTotalOrder; StrictTotalOrder; Preorder)
25+
open import Relation.Binary.Structures
26+
using (IsEquivalence; IsPartialOrder; IsStrictPartialOrder; IsTotalOrder; IsStrictTotalOrder; IsPreorder; IsDecTotalOrder)
27+
open import Relation.Binary.Definitions
28+
using (Irreflexive; _Respects₂_; Antisymmetric; Asymmetric; Symmetric; Transitive; Decidable; Total; Trichotomous)
2329
import Relation.Binary.Construct.NonStrictToStrict as Conv
2430

2531
import Data.List.Relation.Binary.Lex as Core

‎src/Data/List/Relation/Binary/Lex/Strict.agda

+7-1
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,13 @@ open import Data.Sum.Base using (inj₁; inj₂)
1919
open import Data.List.Base using (List; []; _∷_)
2020
open import Level using (_⊔_)
2121
open import Relation.Nullary using (yes; no; ¬_)
22-
open import Relation.Binary
22+
open import Relation.Binary.Core using (Rel; _⇒_)
23+
open import Relation.Binary.Bundles
24+
using (StrictPartialOrder; StrictTotalOrder; Preorder; Poset; DecPoset; DecTotalOrder)
25+
open import Relation.Binary.Structures
26+
using (IsEquivalence; IsStrictPartialOrder; IsStrictTotalOrder; IsPreorder; IsPartialOrder; IsDecPartialOrder; IsTotalOrder; IsDecTotalOrder)
27+
open import Relation.Binary.Definitions
28+
using (Irreflexive; Symmetric; _Respects₂_; Total; Asymmetric; Antisymmetric; Transitive; Trichotomous; Decidable; tri≈; tri<; tri>)
2329
open import Relation.Binary.Consequences
2430
open import Data.List.Relation.Binary.Pointwise as Pointwise
2531
using (Pointwise; []; _∷_; head; tail)

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

+4-1
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,10 @@ open import Data.List.Relation.Binary.Pointwise.Base as Pointwise
1414
open import Data.List.Relation.Binary.Pointwise.Properties as Pointwise
1515
using (symmetric)
1616
open import Level using (Level; _⊔_)
17-
open import Relation.Binary
17+
open import Relation.Binary.Core using (Rel; _⇒_)
18+
open import Relation.Binary.Bundles using (Setoid)
19+
open import Relation.Binary.Structures using (IsEquivalence)
20+
open import Relation.Binary.Definitions using (Reflexive; Symmetric)
1821

1922
private
2023
variable

‎src/Data/List/Relation/Binary/Permutation/Propositional.agda

+4-1
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,10 @@ module Data.List.Relation.Binary.Permutation.Propositional
1010
{a} {A : Set a} where
1111

1212
open import Data.List.Base using (List; []; _∷_)
13-
open import Relation.Binary
13+
open import Relation.Binary.Core using (Rel; _⇒_)
14+
open import Relation.Binary.Bundles using (Setoid)
15+
open import Relation.Binary.Structures using (IsEquivalence)
16+
open import Relation.Binary.Definitions using (Reflexive; Transitive)
1417
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
1518
import Relation.Binary.Reasoning.Setoid as EqReasoning
1619

‎src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda

+2-1
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,8 @@ open import Function.Equality using (_⟨$⟩_)
2727
open import Function.Inverse as Inv using (inverse)
2828
open import Level using (Level)
2929
open import Relation.Unary using (Pred)
30-
open import Relation.Binary
30+
open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_)
31+
open import Relation.Binary.Definitions using (_Respects_; Decidable)
3132
open import Relation.Binary.PropositionalEquality.Core as ≡
3233
using (_≡_ ; refl ; cong; cong₂; _≢_)
3334
open import Relation.Nullary

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

+5-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,11 @@
66

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

9-
open import Relation.Binary
9+
open import Relation.Binary.Core using (Rel; _⇒_)
10+
open import Relation.Binary.Bundles using (Setoid)
11+
open import Relation.Binary.Structures using (IsEquivalence)
12+
open import Relation.Binary.Definitions
13+
using (Reflexive; Symmetric; Transitive)
1014

1115
module Data.List.Relation.Binary.Permutation.Setoid
1216
{a ℓ} (S : Setoid a ℓ) where

‎src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda

+3-1
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,9 @@ open import Function.Base
2525
open import Relation.Nullary.Negation using (¬_)
2626
open import Relation.Nullary.Decidable as Dec using (_×-dec_; yes; no; _because_)
2727
open import Relation.Unary as U using (Pred)
28-
open import Relation.Binary
28+
open import Relation.Binary.Core using (Rel; REL; _⇒_)
29+
open import Relation.Binary.Definitions
30+
using (Trans; Antisym; Irrelevant; Decidable)
2931
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; _≢_)
3032

3133
private

‎src/Data/List/Relation/Binary/Prefix/Homogeneous/Properties.agda

+3-1
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,9 @@ module Data.List.Relation.Binary.Prefix.Homogeneous.Properties where
1010

1111
open import Level
1212
open import Function.Base using (_∘′_)
13-
open import Relation.Binary
13+
open import Relation.Binary.Core using (Rel; REL; _⇒_)
14+
open import Relation.Binary.Structures
15+
using (IsPreorder; IsPartialOrder; IsDecPartialOrder)
1416

1517
open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise)
1618
open import Data.List.Relation.Binary.Prefix.Heterogeneous

‎src/Data/List/Relation/Binary/Sublist/DecPropositional.agda

+3-1
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,9 @@
88

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

11-
open import Relation.Binary
11+
open import Relation.Binary.Bundles using (DecPoset)
12+
open import Relation.Binary.Structures using (IsDecPartialOrder)
13+
open import Relation.Binary.Definitions using (Decidable)
1214
open import Agda.Builtin.Equality using (_≡_)
1315

1416
module Data.List.Relation.Binary.Sublist.DecPropositional

‎src/Data/List/Relation/Binary/Sublist/DecSetoid.agda

+4-1
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,10 @@
88

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

11-
open import Relation.Binary
11+
open import Relation.Binary.Bundles using (DecSetoid; DecPoset)
12+
open import Relation.Binary.Structures
13+
using (IsDecPartialOrder)
14+
open import Relation.Binary.Definitions using (Decidable)
1215

1316
module Data.List.Relation.Binary.Sublist.DecSetoid
1417
{c ℓ} (S : DecSetoid c ℓ) where

0 commit comments

Comments
 (0)