From a356014b4c8474353f201288175fc0064ec3fc93 Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Fri, 29 Mar 2024 17:44:15 -0400
Subject: [PATCH 01/18] Make the main home of `decToMaybe` be
 `Relation.Nullary.Decidable.Core`, but deprecate the one in `Data.Maybe.Base`
 instead of removing it entirely. Fix the library accordingly.

Note that this forces `Relation.Nullary.Decidable.Core` to use `Agda.Builtin.Maybe`
to avoid a cyclic import. This can be fixed once the deprecation is done.
---
 src/Algebra/Solver/CommutativeMonoid.agda     |  4 +--
 .../Solver/IdempotentCommutativeMonoid.agda   |  4 +--
 src/Algebra/Solver/Monoid.agda                |  7 ++---
 src/Data/Graph/Acyclic.agda                   |  6 ++--
 .../Binary/Sublist/Heterogeneous/Solver.agda  | 10 +++----
 src/Data/Maybe/Base.agda                      | 29 ++++++++++++++-----
 src/Relation/Binary/Consequences.agda         |  4 +--
 src/Relation/Nullary/Decidable/Core.agda      | 10 +++++++
 8 files changed, 48 insertions(+), 26 deletions(-)

diff --git a/src/Algebra/Solver/CommutativeMonoid.agda b/src/Algebra/Solver/CommutativeMonoid.agda
index f15f83824f..1127f25bd4 100644
--- a/src/Algebra/Solver/CommutativeMonoid.agda
+++ b/src/Algebra/Solver/CommutativeMonoid.agda
@@ -14,7 +14,7 @@ module Algebra.Solver.CommutativeMonoid {m₁ m₂} (M : CommutativeMonoid m₁
 
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Maybe.Base as Maybe
-  using (Maybe; decToMaybe; From-just; from-just)
+  using (Maybe; From-just; from-just)
 open import Data.Nat as ℕ using (ℕ; zero; suc; _+_)
 open import Data.Nat.GeneralisedArithmetic using (fold)
 open import Data.Product.Base using (_×_; uncurry)
@@ -28,7 +28,7 @@ import Relation.Nullary.Decidable as Dec
 import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
 
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
-open import Relation.Nullary.Decidable using (Dec)
+open import Relation.Nullary.Decidable using (Dec; decToMaybe)
 
 open CommutativeMonoid M
 open ≈-Reasoning setoid
diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
index 35cfcc5ea6..8be6eed4b7 100644
--- a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
+++ b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
@@ -13,7 +13,7 @@ open import Algebra
 open import Data.Bool as Bool using (Bool; true; false; if_then_else_; _∨_)
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Maybe.Base as Maybe
-  using (Maybe; decToMaybe; From-just; from-just)
+  using (Maybe; From-just; from-just)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_)
 open import Data.Product.Base using (_×_; uncurry)
 open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate)
@@ -26,7 +26,7 @@ import Relation.Nullary.Decidable            as Dec
 import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
 
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; decSetoid)
-open import Relation.Nullary.Decidable using (Dec)
+open Dec using (Dec; decToMaybe)
 
 module Algebra.Solver.IdempotentCommutativeMonoid
   {m₁ m₂} (M : IdempotentCommutativeMonoid m₁ m₂) where
diff --git a/src/Algebra/Solver/Monoid.agda b/src/Algebra/Solver/Monoid.agda
index ba6aabee06..9841f1661d 100644
--- a/src/Algebra/Solver/Monoid.agda
+++ b/src/Algebra/Solver/Monoid.agda
@@ -15,7 +15,7 @@ import Data.Fin.Properties as Fin
 open import Data.List.Base hiding (lookup)
 import Data.List.Relation.Binary.Equality.DecPropositional as ListEq
 open import Data.Maybe.Base as Maybe
-  using (Maybe; decToMaybe; From-just; from-just)
+  using (Maybe; From-just; from-just)
 open import Data.Nat.Base using (ℕ)
 open import Data.Product.Base using (_×_; uncurry)
 open import Data.Vec.Base using (Vec; lookup)
@@ -24,8 +24,7 @@ open import Relation.Binary.Definitions using (Decidable)
 
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
 import Relation.Binary.Reflection
-open import Relation.Nullary
-import Relation.Nullary.Decidable as Dec
+import Relation.Nullary.Decidable.Core as Dec
 
 open Monoid M
 open import Relation.Binary.Reasoning.Setoid setoid
@@ -123,7 +122,7 @@ nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂)
 
 prove′ : ∀ {n} (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
 prove′ e₁ e₂ =
-  Maybe.map lemma $ decToMaybe (normalise e₁ ≟ normalise e₂)
+  Maybe.map lemma $ Dec.decToMaybe (normalise e₁ ≟ normalise e₂)
   where
   lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
   lemma eq ρ =
diff --git a/src/Data/Graph/Acyclic.agda b/src/Data/Graph/Acyclic.agda
index bf4c7267b7..47f9163da9 100644
--- a/src/Data/Graph/Acyclic.agda
+++ b/src/Data/Graph/Acyclic.agda
@@ -20,13 +20,13 @@ open import Data.Fin as Fin
   using (Fin; Fin′; zero; suc; #_; toℕ; _≟_; opposite) renaming (_ℕ-ℕ_ to _-_)
 import Data.Fin.Properties as Fin
 open import Data.Product.Base as Prod using (∃; _×_; _,_)
-open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; decToMaybe)
-open import Data.Empty
+open import Data.Maybe.Base as Maybe using (Maybe; nothing; just)
+open import Data.Empty using (⊥)
 open import Data.Unit.Base using (⊤; tt)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Function.Base using (_$_; _∘′_; _∘_; id)
-open import Relation.Nullary
+open import Relation.Nullary.Decidable.Core using (decToMaybe)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 ------------------------------------------------------------------------
diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda
index 86194916f8..a590946a5b 100644
--- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda
@@ -21,7 +21,7 @@ module Data.List.Relation.Binary.Sublist.Heterogeneous.Solver
 
 open import Level using (_⊔_)
 open import Data.Fin as Fin
-open import Data.Maybe.Base as Maybe
+open import Data.Maybe.Base as Maybe using (Maybe; nothing; just)
 open import Data.Nat.Base as ℕ using (ℕ)
 open import Data.Product.Base using (Σ-syntax; _,_)
 open import Data.Vec.Base as Vec using (Vec ; lookup)
@@ -30,11 +30,11 @@ open import Data.List.Properties
 open import Data.List.Relation.Binary.Sublist.Heterogeneous
   hiding (lookup)
 open import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
-open import Function
+open import Function.Base
 
 open import Relation.Binary.PropositionalEquality as ≡
   using (_≡_; _≗_; sym; cong; cong₂; subst₂)
-open import Relation.Nullary
+open import Relation.Nullary.Decidable.Core using (decToMaybe)
 
 open ≡.≡-Reasoning
 
@@ -150,5 +150,5 @@ solveT t u =
 
 -- Prover for ASTs
 
-prove : ∀ {n} (d e : TList n) → From-just (solveT d e)
-prove d e = from-just (solveT d e)
+prove : ∀ {n} (d e : TList n) → Maybe.From-just (solveT d e)
+prove d e = Maybe.from-just (solveT d e)
diff --git a/src/Data/Maybe/Base.agda b/src/Data/Maybe/Base.agda
index b0ae001f46..145816ec78 100644
--- a/src/Data/Maybe/Base.agda
+++ b/src/Data/Maybe/Base.agda
@@ -10,14 +10,12 @@
 
 module Data.Maybe.Base where
 
-open import Level
+open import Level using (Level; Lift)
 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 (_∘_; id; const)
 
 private
   variable
@@ -46,10 +44,6 @@ is-just nothing  = false
 is-nothing : Maybe A → Bool
 is-nothing = not ∘ is-just
 
-decToMaybe : Dec A → Maybe A
-decToMaybe ( true because [a]) = just (invert [a])
-decToMaybe (false because  _ ) = nothing
-
 -- A dependent eliminator.
 
 maybe : ∀ {A : Set a} {B : Maybe A → Set b} →
@@ -137,3 +131,22 @@ thisM a = maybe′ (these a) (this a)
 
 thatM : Maybe A → B → These A B
 thatM = maybe′ these that
+
+------------------------------------------------------------------------
+-- Deprecated
+
+-- Version 2.1
+-- decToMaybe
+
+open import Relation.Nullary.Reflects using (invert)
+open import Relation.Nullary.Decidable.Core
+  using (_because_; Dec)
+
+decToMaybe : Dec A → Maybe A
+decToMaybe ( true because [a]) = just (invert [a])
+decToMaybe (false because  _ ) = nothing
+
+{-# WARNING_ON_USAGE decToMaybe
+"Warning: decToMaybe was deprecated in v2.1.
+Please use Relation.Nullary.Decidable's decToMaybe instead."
+#-}
diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda
index cd560ec995..8b6af958fa 100644
--- a/src/Relation/Binary/Consequences.agda
+++ b/src/Relation/Binary/Consequences.agda
@@ -8,7 +8,7 @@
 
 module Relation.Binary.Consequences where
 
-open import Data.Maybe.Base using (just; nothing; decToMaybe)
+open import Data.Maybe.Base using (just; nothing)
 open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_]′)
 open import Data.Product.Base using (_,_)
 open import Data.Empty.Irrelevant using (⊥-elim)
@@ -17,7 +17,7 @@ open import Level using (Level)
 open import Relation.Binary.Core
 open import Relation.Binary.Definitions
 open import Relation.Nullary using (yes; no; recompute; ¬_)
-open import Relation.Nullary.Decidable.Core using (map′)
+open import Relation.Nullary.Decidable.Core using (map′; decToMaybe)
 open import Relation.Unary using (∁; Pred)
 
 private
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 83da26e51b..2949a6c8ab 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -11,6 +11,9 @@
 
 module Relation.Nullary.Decidable.Core where
 
+-- this can go through `Data.Maybe.Base` once the deprecation of `decToMaybe`
+-- is fully done.
+open import Agda.Builtin.Maybe using (Maybe; just; nothing)
 open import Level using (Level; Lift)
 open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_)
 open import Data.Unit.Polymorphic.Base using (⊤)
@@ -98,6 +101,13 @@ _→-dec_ : Dec A → Dec B → Dec (A → B)
 does  (a? →-dec b?) = not (does a?) ∨ does b?
 proof (a? →-dec b?) = proof a? →-reflects proof b?
 
+------------------------------------------------------------------------
+-- Relationship with Maybe
+
+decToMaybe : Dec A → Maybe A
+decToMaybe ( true because [a]) = just (invert [a])
+decToMaybe (false because  _ ) = nothing
+
 ------------------------------------------------------------------------
 -- Relationship with booleans
 

From bd7f839ddc3bb3e87994e820156e39586dc2ed8e Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Wed, 3 Apr 2024 08:29:38 -0400
Subject: [PATCH 02/18] Update src/Relation/Nullary/Decidable/Core.agda

Good idea.

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
---
 src/Relation/Nullary/Decidable/Core.agda | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 2949a6c8ab..7b5b5174c4 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -11,6 +11,7 @@
 
 module Relation.Nullary.Decidable.Core where
 
+-- decToMaybe was deprecated in v2.1
 -- this can go through `Data.Maybe.Base` once the deprecation of `decToMaybe`
 -- is fully done.
 open import Agda.Builtin.Maybe using (Maybe; just; nothing)

From 603fe22ddf0c0b5ab825db80efecc72b6a02ad45 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 8 Apr 2024 15:38:46 +0100
Subject: [PATCH 03/18] simplified the deprecation

---
 src/Data/Maybe/Base.agda | 12 +++---------
 1 file changed, 3 insertions(+), 9 deletions(-)

diff --git a/src/Data/Maybe/Base.agda b/src/Data/Maybe/Base.agda
index 145816ec78..c208f59cca 100644
--- a/src/Data/Maybe/Base.agda
+++ b/src/Data/Maybe/Base.agda
@@ -16,6 +16,7 @@ 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 using (_∘_; id; const)
+import Relation.Nullary.Decidable.Core
 
 private
   variable
@@ -138,15 +139,8 @@ thatM = maybe′ these that
 -- Version 2.1
 -- decToMaybe
 
-open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary.Decidable.Core
-  using (_because_; Dec)
-
-decToMaybe : Dec A → Maybe A
-decToMaybe ( true because [a]) = just (invert [a])
-decToMaybe (false because  _ ) = nothing
-
+decToMaybe = Relation.Nullary.Decidable.Core.decToMaybe
 {-# WARNING_ON_USAGE decToMaybe
 "Warning: decToMaybe was deprecated in v2.1.
-Please use Relation.Nullary.Decidable's decToMaybe instead."
+Please use Relation.Nullary.Decidable.Core.decToMaybe instead."
 #-}

From abbc08bd61da54fa4720cd7774dd9fafda2e8ec4 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 8 Apr 2024 15:44:28 +0100
Subject: [PATCH 04/18] `CHANGELOG`

---
 CHANGELOG.md | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2b9d357511..4a47dfaf58 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -49,6 +49,11 @@ Deprecated names
   _-_  ↦  _//_
   ```
 
+* In `Data.Maybe.Base`:
+  ```agda
+  decToMaybe  ↦  Relation.Nullary.Decidable.Core.decToMaybe
+  ```
+
 * In `Data.Nat.Divisibility.Core`:
   ```agda
   *-pres-∣  ↦  Data.Nat.Divisibility.*-pres-∣
@@ -399,6 +404,11 @@ Additions to existing modules
   ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋
   ```
 
+* Added new proof in `Relation.Nullary.Decidable.Core`:
+  ```agda
+  decToMaybe : Dec A → Maybe A
+  ```
+
 * Added new definitions in `Relation.Unary`
   ```
   Stable          : Pred A ℓ → Set _

From 2c6d6e9a532d8aa2adaffecc9630ec2b97f92aba Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 26 Apr 2024 09:06:44 +0100
Subject: [PATCH 05/18] narrowed import too far

---
 src/Algebra/Solver/IdempotentCommutativeMonoid.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
index d1d7b2864a..6991f44653 100644
--- a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
+++ b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
@@ -26,7 +26,7 @@ import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
 
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
-open import Relation.Nullary.Decidable.Core as Dec using (Dec; decToMaybe)
+open import Relation.Nullary.Decidable as Dec using (Dec; decToMaybe)
 
 
 module Algebra.Solver.IdempotentCommutativeMonoid

From 7712d985e83fb7f16a17acf01ac7382521540148 Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Thu, 2 May 2024 22:24:41 -0400
Subject: [PATCH 06/18] tweak a couple of the solvers for consistency, as per
 suggestions.

---
 src/Algebra/Solver/IdempotentCommutativeMonoid.agda  |  4 ++--
 .../Binary/Sublist/Heterogeneous/Solver.agda         | 12 ++++++------
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
index 6991f44653..a3e37b0e2f 100644
--- a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
+++ b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
@@ -26,7 +26,7 @@ import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
 
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
-open import Relation.Nullary.Decidable as Dec using (Dec; decToMaybe)
+open import Relation.Nullary.Decidable as Dec using (Dec)
 
 
 module Algebra.Solver.IdempotentCommutativeMonoid
@@ -198,7 +198,7 @@ nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable Bool._≟_ nf₁ nf₂)
 
 prove′ : (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
 prove′ e₁ e₂ =
-  Maybe.map lemma (decToMaybe (normalise e₁ ≟ normalise e₂))
+  Maybe.map lemma (Dec.decToMaybe (normalise e₁ ≟ normalise e₂))
   where
   lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
   lemma eq ρ =
diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda
index 5243276bc0..6847de90e0 100644
--- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda
@@ -21,7 +21,7 @@ module Data.List.Relation.Binary.Sublist.Heterogeneous.Solver
 
 open import Level using (_⊔_)
 open import Data.Fin as Fin
-open import Data.Maybe.Base as Maybe using (Maybe; nothing; just)
+open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; From-just; from-just)
 open import Data.Nat.Base as ℕ using (ℕ)
 open import Data.Product.Base using (Σ-syntax; _,_)
 open import Data.Vec.Base as Vec using (Vec ; lookup)
@@ -35,7 +35,7 @@ open import Function.Base using (_$_; case_of_)
 open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; _≗_; sym; cong; cong₂; subst₂)
 open import Relation.Binary.PropositionalEquality.Properties as ≡
-open import Relation.Nullary.Decidable.Core using (decToMaybe)
+import Relation.Nullary.Decidable.Core as Dec
 
 open ≡.≡-Reasoning
 
@@ -125,8 +125,8 @@ private
 
 -- Solver for items
 solveI : ∀ {n} (a b : Item n) → Maybe (a ⊆I b)
-solveI (var k) (var l) = Maybe.map var $ decToMaybe (k Fin.≟ l)
-solveI (val a) (val b) = Maybe.map val $ decToMaybe (R? a b)
+solveI (var k) (var l) = Maybe.map var $ Dec.decToMaybe (k Fin.≟ l)
+solveI (val a) (val b) = Maybe.map val $ Dec.decToMaybe (R? a b)
 solveI _ _ = nothing
 
 -- Solver for linearised expressions
@@ -151,5 +151,5 @@ solveT t u =
 
 -- Prover for ASTs
 
-prove : ∀ {n} (d e : TList n) → Maybe.From-just (solveT d e)
-prove d e = Maybe.from-just (solveT d e)
+prove : ∀ {n} (d e : TList n) → From-just (solveT d e)
+prove d e = from-just (solveT d e)

From 256a50589dacab913c69f4db5b4570b46cf440d7 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Jun 2024 09:15:07 +0100
Subject: [PATCH 07/18] chnage to `public` re-export of
 `Relation.Nullary.Decidable.Core.decToMaybe`

---
 CHANGELOG.md                             |  2 +-
 src/Data/Maybe/Base.agda                 | 11 +++++++----
 src/Relation/Nullary/Decidable/Core.agda |  2 +-
 3 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9027e09ab5..342420f111 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -744,7 +744,7 @@ Additions to existing modules
   recompute          : Reflects A b → Recomputable A
   recompute-constant : (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q
  ```
- 
+
 * Added new definitions in `Relation.Unary`
   ```
   Stable          : Pred A ℓ → Set _
diff --git a/src/Data/Maybe/Base.agda b/src/Data/Maybe/Base.agda
index c208f59cca..2bc9a6a7d6 100644
--- a/src/Data/Maybe/Base.agda
+++ b/src/Data/Maybe/Base.agda
@@ -16,7 +16,7 @@ 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 using (_∘_; id; const)
-import Relation.Nullary.Decidable.Core
+import Relation.Nullary.Decidable.Core as Dec
 
 private
   variable
@@ -134,12 +134,15 @@ thatM : Maybe A → B → These A B
 thatM = maybe′ these that
 
 ------------------------------------------------------------------------
--- Deprecated
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
 
 -- Version 2.1
--- decToMaybe
+-- decToMaybe #2330/2336
 
-decToMaybe = Relation.Nullary.Decidable.Core.decToMaybe
+open Dec public using (decToMaybe)
 {-# WARNING_ON_USAGE decToMaybe
 "Warning: decToMaybe was deprecated in v2.1.
 Please use Relation.Nullary.Decidable.Core.decToMaybe instead."
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 32f0464324..429331dad0 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -11,7 +11,7 @@
 
 module Relation.Nullary.Decidable.Core where
 
--- decToMaybe was intended to be deprecated in v2.1 #2330/#2336
+-- decToMaybe was deprecated in v2.1 #2330/#2336
 -- this can go through `Data.Maybe.Base` once that deprecation is fully done.
 open import Agda.Builtin.Maybe using (Maybe; just; nothing)
 

From 4428f966334bdd496f0e39f29f5fd5c568de1370 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Jun 2024 14:45:28 +0100
Subject: [PATCH 08/18] Revert "chnage to `public` re-export of
 `Relation.Nullary.Decidable.Core.decToMaybe`"

This reverts commit 256a50589dacab913c69f4db5b4570b46cf440d7.
---
 CHANGELOG.md                             |  2 +-
 src/Data/Maybe/Base.agda                 | 11 ++++-------
 src/Relation/Nullary/Decidable/Core.agda |  2 +-
 3 files changed, 6 insertions(+), 9 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 342420f111..9027e09ab5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -744,7 +744,7 @@ Additions to existing modules
   recompute          : Reflects A b → Recomputable A
   recompute-constant : (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q
  ```
-
+ 
 * Added new definitions in `Relation.Unary`
   ```
   Stable          : Pred A ℓ → Set _
diff --git a/src/Data/Maybe/Base.agda b/src/Data/Maybe/Base.agda
index 2bc9a6a7d6..c208f59cca 100644
--- a/src/Data/Maybe/Base.agda
+++ b/src/Data/Maybe/Base.agda
@@ -16,7 +16,7 @@ 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 using (_∘_; id; const)
-import Relation.Nullary.Decidable.Core as Dec
+import Relation.Nullary.Decidable.Core
 
 private
   variable
@@ -134,15 +134,12 @@ thatM : Maybe A → B → These A B
 thatM = maybe′ these that
 
 ------------------------------------------------------------------------
--- DEPRECATED NAMES
-------------------------------------------------------------------------
--- Please use the new names as continuing support for the old names is
--- not guaranteed.
+-- Deprecated
 
 -- Version 2.1
--- decToMaybe #2330/2336
+-- decToMaybe
 
-open Dec public using (decToMaybe)
+decToMaybe = Relation.Nullary.Decidable.Core.decToMaybe
 {-# WARNING_ON_USAGE decToMaybe
 "Warning: decToMaybe was deprecated in v2.1.
 Please use Relation.Nullary.Decidable.Core.decToMaybe instead."
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 429331dad0..32f0464324 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -11,7 +11,7 @@
 
 module Relation.Nullary.Decidable.Core where
 
--- decToMaybe was deprecated in v2.1 #2330/#2336
+-- decToMaybe was intended to be deprecated in v2.1 #2330/#2336
 -- this can go through `Data.Maybe.Base` once that deprecation is fully done.
 open import Agda.Builtin.Maybe using (Maybe; just; nothing)
 

From 1eb511d0117d32c40610be15c2cd5d07855ebe58 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Jun 2024 14:59:55 +0100
Subject: [PATCH 09/18] `fix-whitespace`

---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9027e09ab5..342420f111 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -744,7 +744,7 @@ Additions to existing modules
   recompute          : Reflects A b → Recomputable A
   recompute-constant : (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q
  ```
- 
+
 * Added new definitions in `Relation.Unary`
   ```
   Stable          : Pred A ℓ → Set _

From 7a2b429be79d574be6f16bc98869d440d05fdda4 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Jun 2024 15:05:59 +0100
Subject: [PATCH 10/18] simplify `import`s

---
 src/Relation/Binary/Consequences.agda | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda
index 8b6af958fa..0065f41d96 100644
--- a/src/Relation/Binary/Consequences.agda
+++ b/src/Relation/Binary/Consequences.agda
@@ -8,16 +8,16 @@
 
 module Relation.Binary.Consequences where
 
-open import Data.Maybe.Base using (just; nothing)
-open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_]′)
+open import Data.Empty using (⊥-elim)
 open import Data.Product.Base using (_,_)
-open import Data.Empty.Irrelevant using (⊥-elim)
+open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_]′)
 open import Function.Base using (_∘_; _∘₂_; _$_; flip)
 open import Level using (Level)
 open import Relation.Binary.Core
 open import Relation.Binary.Definitions
-open import Relation.Nullary using (yes; no; recompute; ¬_)
-open import Relation.Nullary.Decidable.Core using (map′; decToMaybe)
+open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Nullary.Decidable.Core
+  using (yes; no; recompute; map′; decToMaybe)
 open import Relation.Unary using (∁; Pred)
 
 private

From 7a3644b030f97a03a442c0d4dc1944cdc32b6467 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Jun 2024 15:18:39 +0100
Subject: [PATCH 11/18] make consistent with `Idempotent` case

---
 src/Algebra/Solver/CommutativeMonoid.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Algebra/Solver/CommutativeMonoid.agda b/src/Algebra/Solver/CommutativeMonoid.agda
index 1127f25bd4..6f8ff12346 100644
--- a/src/Algebra/Solver/CommutativeMonoid.agda
+++ b/src/Algebra/Solver/CommutativeMonoid.agda
@@ -28,7 +28,7 @@ import Relation.Nullary.Decidable as Dec
 import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
 
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
-open import Relation.Nullary.Decidable using (Dec; decToMaybe)
+open import Relation.Nullary.Decidable as Dec using (Dec)
 
 open CommutativeMonoid M
 open ≈-Reasoning setoid
@@ -184,7 +184,7 @@ nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable ℕ._≟_ nf₁ nf₂)
 
 prove′ : (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
 prove′ e₁ e₂ =
-  Maybe.map lemma (decToMaybe (normalise e₁ ≟ normalise e₂))
+  Maybe.map lemma (Dec.decToMaybe (normalise e₁ ≟ normalise e₂))
   where
   lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
   lemma eq ρ =

From 13160dc539307ddd278d176abb798cbbab0943e0 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Jun 2024 15:36:07 +0100
Subject: [PATCH 12/18] tidy up

---
 src/Relation/Nullary/Decidable/Core.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 32f0464324..c2eca3162a 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -11,12 +11,12 @@
 
 module Relation.Nullary.Decidable.Core where
 
--- decToMaybe was intended to be deprecated in v2.1 #2330/#2336
+-- decToMaybe was deprecated in v2.1 #2330/#2336
 -- this can go through `Data.Maybe.Base` once that deprecation is fully done.
 open import Agda.Builtin.Maybe using (Maybe; just; nothing)
 
 open import Agda.Builtin.Equality using (_≡_)
-open import Level using (Level; Lift)
+open import Level using (Level)
 open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_)
 open import Data.Unit.Polymorphic.Base using (⊤)
 open import Data.Product.Base using (_×_)

From 710b25a030e30cf7eaac296b6564be536df51917 Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Thu, 6 Jun 2024 22:51:26 -0400
Subject: [PATCH 13/18] instead of an alias, open public so that Agda knows
 these really are the same. This is a better deprecation strategy.

---
 src/Data/Maybe/Base.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Maybe/Base.agda b/src/Data/Maybe/Base.agda
index c208f59cca..1e93044c06 100644
--- a/src/Data/Maybe/Base.agda
+++ b/src/Data/Maybe/Base.agda
@@ -16,7 +16,7 @@ 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 using (_∘_; id; const)
-import Relation.Nullary.Decidable.Core
+import Relation.Nullary.Decidable.Core as Dec
 
 private
   variable
@@ -139,7 +139,7 @@ thatM = maybe′ these that
 -- Version 2.1
 -- decToMaybe
 
-decToMaybe = Relation.Nullary.Decidable.Core.decToMaybe
+open Dec using (decToMaybe) public
 {-# WARNING_ON_USAGE decToMaybe
 "Warning: decToMaybe was deprecated in v2.1.
 Please use Relation.Nullary.Decidable.Core.decToMaybe instead."

From 70e2916eaa3a38500495f971bb8f0f8fab3635dc Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sun, 9 Jun 2024 08:51:45 +0100
Subject: [PATCH 14/18] rename(provisional)+deprecate

---
 src/Relation/Nullary/Decidable/Core.agda | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index c2eca3162a..edeb5d29ce 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -110,9 +110,9 @@ proof (a? →-dec b?) = proof a? →-reflects proof b?
 ------------------------------------------------------------------------
 -- Relationship with Maybe
 
-decToMaybe : Dec A → Maybe A
-decToMaybe ( true because [a]) = just (invert [a])
-decToMaybe (false because  _ ) = nothing
+dec⇒maybe : Dec A → Maybe A
+dec⇒maybe ( true because [a]) = just (invert [a])
+dec⇒maybe (false because  _ ) = nothing
 
 ------------------------------------------------------------------------
 -- Relationship with booleans
@@ -212,3 +212,12 @@ excluded-middle = ¬¬-excluded-middle
 "Warning: excluded-middle was deprecated in v2.0.
 Please use ¬¬-excluded-middle instead."
 #-}
+
+-- Version 2.1
+
+decToMaybe = dec⇒maybe
+{-# WARNING_ON_USAGE decToMaybe
+"Warning: decToMaybe was deprecated in v2.1.
+Please use Relation.Nullary.Decidable.Core.dec⇒maybe instead."
+#-}
+

From 1c82a463babb2a2377bb1eb42a7cd67e2af35583 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sun, 9 Jun 2024 08:52:39 +0100
Subject: [PATCH 15/18] knock-on

---
 src/Relation/Binary/Consequences.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda
index 0065f41d96..3cdb4db356 100644
--- a/src/Relation/Binary/Consequences.agda
+++ b/src/Relation/Binary/Consequences.agda
@@ -17,7 +17,7 @@ open import Relation.Binary.Core
 open import Relation.Binary.Definitions
 open import Relation.Nullary.Negation.Core using (¬_)
 open import Relation.Nullary.Decidable.Core
-  using (yes; no; recompute; map′; decToMaybe)
+  using (yes; no; recompute; map′; dec⇒maybe)
 open import Relation.Unary using (∁; Pred)
 
 private
@@ -193,7 +193,7 @@ module _  {_R_ : Rel A ℓ₁} {Q : Rel A ℓ₂} where
 module _ {R : REL A B p} where
 
   dec⇒weaklyDec : Decidable R → WeaklyDecidable R
-  dec⇒weaklyDec dec x y = decToMaybe (dec x y)
+  dec⇒weaklyDec dec x y = dec⇒maybe (dec x y)
 
   dec⇒recomputable : Decidable R → Recomputable R
   dec⇒recomputable dec {a} {b} = recompute $ dec a b

From 06c4072188912e42fac93ec7e507474e81e1ab36 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sun, 9 Jun 2024 09:14:43 +0100
Subject: [PATCH 16/18] =?UTF-8?q?knock-on:=20refactor=20via=20`dec?=
 =?UTF-8?q?=E2=87=92maybe`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Algebra/Solver/CommutativeMonoid.agda                   | 3 ++-
 src/Algebra/Solver/IdempotentCommutativeMonoid.agda         | 3 ++-
 src/Algebra/Solver/Monoid.agda                              | 3 ++-
 src/Data/Graph/Acyclic.agda                                 | 6 +++---
 .../List/Relation/Binary/Sublist/Heterogeneous/Solver.agda  | 6 +++---
 5 files changed, 12 insertions(+), 9 deletions(-)

diff --git a/src/Algebra/Solver/CommutativeMonoid.agda b/src/Algebra/Solver/CommutativeMonoid.agda
index 6f8ff12346..04d4d372e6 100644
--- a/src/Algebra/Solver/CommutativeMonoid.agda
+++ b/src/Algebra/Solver/CommutativeMonoid.agda
@@ -27,6 +27,7 @@ import Relation.Binary.Reflection as Reflection
 import Relation.Nullary.Decidable as Dec
 import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
 
+open import Relation.Binary.Consequences using (dec⇒weaklyDec)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Nullary.Decidable as Dec using (Dec)
 
@@ -184,7 +185,7 @@ nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable ℕ._≟_ nf₁ nf₂)
 
 prove′ : (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
 prove′ e₁ e₂ =
-  Maybe.map lemma (Dec.decToMaybe (normalise e₁ ≟ normalise e₂))
+  Maybe.map lemma (dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂))
   where
   lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
   lemma eq ρ =
diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
index a3e37b0e2f..00b8824975 100644
--- a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
+++ b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
@@ -24,6 +24,7 @@ import Relation.Binary.Reasoning.Setoid  as ≈-Reasoning
 import Relation.Binary.Reflection            as Reflection
 import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
 
+open import Relation.Binary.Consequences using (dec⇒weaklyDec)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 open import Relation.Nullary.Decidable as Dec using (Dec)
@@ -198,7 +199,7 @@ nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable Bool._≟_ nf₁ nf₂)
 
 prove′ : (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
 prove′ e₁ e₂ =
-  Maybe.map lemma (Dec.decToMaybe (normalise e₁ ≟ normalise e₂))
+  Maybe.map lemma (dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂))
   where
   lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
   lemma eq ρ =
diff --git a/src/Algebra/Solver/Monoid.agda b/src/Algebra/Solver/Monoid.agda
index 5630a9c63d..7debc4e1aa 100644
--- a/src/Algebra/Solver/Monoid.agda
+++ b/src/Algebra/Solver/Monoid.agda
@@ -20,6 +20,7 @@ open import Data.Nat.Base using (ℕ)
 open import Data.Product.Base using (_×_; uncurry)
 open import Data.Vec.Base using (Vec; lookup)
 open import Function.Base using (_∘_; _$_)
+open import Relation.Binary.Consequences using (dec⇒weaklyDec)
 open import Relation.Binary.Definitions using (DecidableEquality)
 
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
@@ -122,7 +123,7 @@ nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂)
 
 prove′ : ∀ {n} (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
 prove′ e₁ e₂ =
-  Maybe.map lemma $ Dec.decToMaybe (normalise e₁ ≟ normalise e₂)
+  Maybe.map lemma $ dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂)
   where
   lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
   lemma eq ρ =
diff --git a/src/Data/Graph/Acyclic.agda b/src/Data/Graph/Acyclic.agda
index 47f9163da9..451581bf4e 100644
--- a/src/Data/Graph/Acyclic.agda
+++ b/src/Data/Graph/Acyclic.agda
@@ -20,13 +20,13 @@ open import Data.Fin as Fin
   using (Fin; Fin′; zero; suc; #_; toℕ; _≟_; opposite) renaming (_ℕ-ℕ_ to _-_)
 import Data.Fin.Properties as Fin
 open import Data.Product.Base as Prod using (∃; _×_; _,_)
-open import Data.Maybe.Base as Maybe using (Maybe; nothing; just)
+open import Data.Maybe.Base as Maybe using (Maybe)
 open import Data.Empty using (⊥)
 open import Data.Unit.Base using (⊤; tt)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Function.Base using (_$_; _∘′_; _∘_; id)
-open import Relation.Nullary.Decidable.Core using (decToMaybe)
+open import Relation.Binary.Consequences using (dec⇒weaklyDec)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 ------------------------------------------------------------------------
@@ -238,7 +238,7 @@ preds (c & g) (suc i) =
             (List.map (Prod.map suc id) $ preds g i)
   where
   p : ∀ {e} {E : Set e} {n} (i : Fin n) → E × Fin n → Maybe (Fin′ (suc i) × E)
-  p i (e , j) = Maybe.map (λ{ refl → zero , e }) (decToMaybe (i ≟ j))
+  p i (e , j) = Maybe.map (λ{ refl → zero , e }) (dec⇒weaklyDec _≟_ i j)
 
 private
 
diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda
index 6847de90e0..11db87fa52 100644
--- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda
@@ -32,10 +32,10 @@ open import Data.List.Relation.Binary.Sublist.Heterogeneous
 open import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
 open import Function.Base using (_$_; case_of_)
 
+open import Relation.Binary.Consequences using (dec⇒weaklyDec)
 open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; _≗_; sym; cong; cong₂; subst₂)
 open import Relation.Binary.PropositionalEquality.Properties as ≡
-import Relation.Nullary.Decidable.Core as Dec
 
 open ≡.≡-Reasoning
 
@@ -125,8 +125,8 @@ private
 
 -- Solver for items
 solveI : ∀ {n} (a b : Item n) → Maybe (a ⊆I b)
-solveI (var k) (var l) = Maybe.map var $ Dec.decToMaybe (k Fin.≟ l)
-solveI (val a) (val b) = Maybe.map val $ Dec.decToMaybe (R? a b)
+solveI (var k) (var l) = Maybe.map var $ dec⇒weaklyDec Fin._≟_ k  l
+solveI (val a) (val b) = Maybe.map val $ dec⇒weaklyDec R? a b
 solveI _ _ = nothing
 
 -- Solver for linearised expressions

From aeb212c5e7ffd3386c12084ef2d6828ba7ddd55b Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sun, 9 Jun 2024 09:26:22 +0100
Subject: [PATCH 17/18] deprecation via delegation

---
 src/Data/Maybe/Base.agda | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/Data/Maybe/Base.agda b/src/Data/Maybe/Base.agda
index 1e93044c06..447280b9dd 100644
--- a/src/Data/Maybe/Base.agda
+++ b/src/Data/Maybe/Base.agda
@@ -134,13 +134,12 @@ thatM : Maybe A → B → These A B
 thatM = maybe′ these that
 
 ------------------------------------------------------------------------
--- Deprecated
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
 
 -- Version 2.1
 -- decToMaybe
 
 open Dec using (decToMaybe) public
-{-# WARNING_ON_USAGE decToMaybe
-"Warning: decToMaybe was deprecated in v2.1.
-Please use Relation.Nullary.Decidable.Core.decToMaybe instead."
-#-}

From 522053d94c73375e6a5f6f075f86df25e706e64e Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sun, 9 Jun 2024 09:29:59 +0100
Subject: [PATCH 18/18] fix `CHANGELOG`

---
 CHANGELOG.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 342420f111..79f9103502 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -66,7 +66,7 @@ Deprecated names
 
 * In `Data.Maybe.Base`:
   ```agda
-  decToMaybe  ↦  Relation.Nullary.Decidable.Core.decToMaybe
+  decToMaybe  ↦  Relation.Nullary.Decidable.Core.dec⇒maybe
   ```
 
 * In `Algebra.Structures.Biased`:
@@ -723,9 +723,9 @@ Additions to existing modules
   WeaklyDecidable : Set _
   ```
 
-* Added new proof in `Relation.Nullary.Decidable.Core`:
+* Added new definition and proof in `Relation.Nullary.Decidable.Core`:
   ```agda
-  decToMaybe : Dec A → Maybe A
+  dec⇒maybe : Dec A → Maybe A
   recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q
   ```