Skip to content

Commit f3fb598

Browse files
jamesmckinnajamesmckinna
authored
Systematise use of Relation.Binary.Definitions.DecidableEquality (#2354)
* systematic use of `DecidableEquality` * tweak
1 parent 4676ad7 commit f3fb598

File tree

23 files changed

+56
-59
lines changed

23 files changed

+56
-59
lines changed

‎src/Algebra/Solver/Monoid.agda

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ open import Data.Nat.Base using (ℕ)
2020
open import Data.Product.Base using (_×_; uncurry)
2121
open import Data.Vec.Base using (Vec; lookup)
2222
open import Function.Base using (_∘_; _$_)
23-
open import Relation.Binary.Definitions using (Decidable)
23+
open import Relation.Binary.Definitions using (DecidableEquality)
2424

2525
open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
2626
import Relation.Binary.Reflection
@@ -114,7 +114,7 @@ open module R = Relation.Binary.Reflection
114114

115115
infix 5 _≟_
116116

117-
_≟_ : ∀ {n} → Decidable {A = Normal n} _≡_
117+
_≟_ : ∀ {n} → DecidableEquality (Normal n)
118118
nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂)
119119
where open ListEq Fin._≟_
120120

‎src/Axiom/UniquenessOfIdentityProofs.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,7 @@ module Constant⇒UIP
6060
-- proof produced by the decision procedure.
6161

6262
module Decidable⇒UIP
63-
{a} {A : Set a} (_≟_ : Decidable {A = A} _≡_)
63+
{a} {A : Set a} (_≟_ : DecidableEquality A)
6464
where
6565

6666
≡-normalise : _≡_ {A = A} ⇒ _≡_

‎src/Data/Bool/Properties.agda

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ open import Relation.Binary.Structures
2525
open import Relation.Binary.Bundles
2626
using (Setoid; DecSetoid; Poset; Preorder; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder)
2727
open import Relation.Binary.Definitions
28-
using (Decidable; Reflexive; Transitive; Antisymmetric; Minimum; Maximum; Total; Irrelevant; Irreflexive; Asymmetric; Trans; Trichotomous; tri≈; tri<; tri>; _Respects₂_)
28+
using (Decidable; DecidableEquality; Reflexive; Transitive; Antisymmetric; Minimum; Maximum; Total; Irrelevant; Irreflexive; Asymmetric; Trans; Trichotomous; tri≈; tri<; tri>; _Respects₂_)
2929
open import Relation.Binary.PropositionalEquality.Core
3030
open import Relation.Binary.PropositionalEquality.Properties
3131
open import Relation.Nullary.Decidable.Core using (True; yes; no; fromWitness)
@@ -48,7 +48,7 @@ private
4848

4949
infix 4 _≟_
5050

51-
_≟_ : Decidable {A = Bool} _≡_
51+
_≟_ : DecidableEquality Bool
5252
true ≟ true = yes refl
5353
false ≟ false = yes refl
5454
true ≟ false = no λ()

‎src/Data/Char/Properties.agda

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ open import Relation.Binary.Bundles
2323
open import Relation.Binary.Structures
2424
using (IsDecEquivalence; IsStrictPartialOrder; IsStrictTotalOrder; IsPreorder; IsPartialOrder; IsDecPartialOrder; IsEquivalence)
2525
open import Relation.Binary.Definitions
26-
using (Decidable; Trichotomous; Irreflexive; Transitive; Asymmetric; Antisymmetric; Symmetric; Substitutive; Reflexive; tri<; tri≈; tri>)
26+
using (Decidable; DecidableEquality; Trichotomous; Irreflexive; Transitive; Asymmetric; Antisymmetric; Symmetric; Substitutive; Reflexive; tri<; tri≈; tri>)
2727
import Relation.Binary.Construct.On as On
2828
import Relation.Binary.Construct.Subst.Equality as Subst
2929
import Relation.Binary.Construct.Closure.Reflexive as Refl
@@ -55,7 +55,7 @@ open import Agda.Builtin.Char.Properties
5555
-- Properties of _≡_
5656

5757
infix 4 _≟_
58-
_≟_ : Decidable {A = Char} _≡_
58+
_≟_ : DecidableEquality Char
5959
x ≟ y = map′ ≈⇒≡ ≈-reflexive (toℕ x ℕ.≟ toℕ y)
6060

6161
setoid : Setoid _ _

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,12 +6,12 @@
66

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

9-
open import Relation.Binary.Definitions using (Decidable)
10-
open import Relation.Binary.PropositionalEquality using (_≡_)
11-
open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
9+
open import Relation.Binary.Definitions using (DecidableEquality)
1210

1311
module Data.List.Membership.DecPropositional
14-
{a} {A : Set a} (_≟_ : Decidable (_≡_ {A = A})) where
12+
{a} {A : Set a} (_≟_ : DecidableEquality A) where
13+
14+
open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
1515

1616
------------------------------------------------------------------------
1717
-- Re-export contents of propositional membership

‎src/Data/List/Membership/Propositional/Properties.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -259,7 +259,7 @@ module _ {r} {R : Rel A r} (R? : Binary.Decidable R) where
259259
∈-deduplicate⁻ : ∀ xs {z} → z ∈ deduplicate R? xs → z ∈ xs
260260
∈-deduplicate⁻ xs z∈dedup[R,xs] = Membership.∈-deduplicate⁻ (≡.setoid A) R? xs z∈dedup[R,xs]
261261

262-
module _ (_≈?_ : Binary.Decidable {A = A} _≡_) where
262+
module _ (_≈?_ : DecidableEquality A) where
263263

264264
∈-derun⁺ : ∀ {xs z} → z ∈ xs → z ∈ derun _≈?_ xs
265265
∈-derun⁺ z∈xs = Membership.∈-derun⁺ (≡.setoid A) _≈?_ (flip trans) z∈xs

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -10,16 +10,16 @@
1010

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

13-
open import Relation.Binary.Definitions using (Decidable)
14-
open import Relation.Binary.PropositionalEquality
13+
open import Relation.Binary.Definitions using (DecidableEquality)
1514

1615
module Data.List.Relation.Binary.Equality.DecPropositional
17-
{a} {A : Set a} (_≟_ : Decidable {A = A} _≡_) where
16+
{a} {A : Set a} (_≟_ : DecidableEquality A) where
1817

1918
open import Data.List.Base using (List)
2019
open import Data.List.Properties using (≡-dec)
2120
import Data.List.Relation.Binary.Equality.Propositional as PropositionalEq
2221
import Data.List.Relation.Binary.Equality.DecSetoid as DecSetoidEq
22+
open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
2323

2424
------------------------------------------------------------------------
2525
-- Publically re-export everything from decSetoid and propositional
@@ -34,5 +34,5 @@ open DecSetoidEq (decSetoid _≟_) public
3434

3535
infix 4 _≡?_
3636

37-
_≡?_ : Decidable (_≡_ {A = List A})
37+
_≡?_ : DecidableEquality (List A)
3838
_≡?_ = ≡-dec _≟_

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

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -8,19 +8,18 @@
88

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

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

1613
module Data.List.Relation.Binary.Sublist.DecPropositional
17-
{a} {A : Set a} (_≟_ : Decidable {A = A} _≡_)
14+
{a} {A : Set a} (_≟_ : DecidableEquality A)
1815
where
1916

2017
open import Data.List.Relation.Binary.Equality.DecPropositional _≟_
2118
using (_≡?_)
2219
import Data.List.Relation.Binary.Sublist.DecSetoid as DecSetoidSublist
2320
import Data.List.Relation.Binary.Sublist.Propositional as PropositionalSublist
21+
open import Relation.Binary.Bundles using (DecPoset)
22+
open import Relation.Binary.Structures using (IsDecPartialOrder)
2423
open import Relation.Binary.PropositionalEquality
2524

2625
------------------------------------------------------------------------

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

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -7,13 +7,12 @@
77

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

10-
open import Relation.Binary.Definitions using (Decidable)
11-
open import Relation.Binary.PropositionalEquality.Core using (_≡_)
10+
open import Relation.Binary.Definitions using (DecidableEquality)
1211

1312
module Data.List.Relation.Binary.Sublist.DecPropositional.Solver
14-
{a} {A : Set a} (_≟_ : Decidable {A = A} _≡_)
13+
{a} {A : Set a} (_≟_ : DecidableEquality A)
1514
where
1615

17-
import Relation.Binary.PropositionalEquality.Properties as P
16+
open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
1817

19-
open import Data.List.Relation.Binary.Sublist.DecSetoid.Solver (P.decSetoid _≟_) public
18+
open import Data.List.Relation.Binary.Sublist.DecSetoid.Solver (decSetoid _≟_) public

‎src/Data/Maybe/Properties.agda

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ open import Data.Product.Base using (_,_)
1717
open import Function.Base using (_∋_; id; _∘_; _∘′_)
1818
open import Function.Definitions using (Injective)
1919
open import Level using (Level)
20-
open import Relation.Binary.Definitions using (Decidable)
20+
open import Relation.Binary.Definitions using (DecidableEquality)
2121
open import Relation.Binary.PropositionalEquality
2222
open import Relation.Nullary.Decidable using (yes; no)
2323
open import Relation.Nullary.Decidable using (map′)
@@ -35,7 +35,7 @@ private
3535
just-injective : ∀ {x y} → (Maybe A ∋ just x) ≡ just y → x ≡ y
3636
just-injective refl = refl
3737

38-
≡-dec : Decidable _≡_ → Decidable {A = Maybe A} _≡_
38+
≡-dec : DecidableEquality A → DecidableEquality (Maybe A)
3939
≡-dec _≟_ nothing nothing = yes refl
4040
≡-dec _≟_ (just x) nothing = no λ()
4141
≡-dec _≟_ nothing (just y) = no λ()

0 commit comments

Comments
 (0)