Skip to content

[ refactor ] v2.4-admissible version of #2952#2980

Merged
Taneb merged 32 commits into
agda:masterfrom
jamesmckinna:issue2845-v2.4
Jun 8, 2026
Merged

[ refactor ] v2.4-admissible version of #2952#2980
Taneb merged 32 commits into
agda:masterfrom
jamesmckinna:issue2845-v2.4

Conversation

@jamesmckinna

@jamesmckinna jamesmckinna commented Apr 16, 2026

Copy link
Copy Markdown
Collaborator

Cf. #2952 (comment)
NB. This is based off #2952 but without the fieldame change, so any review comments there should carry over here, mutatis mutandis...

This PR attacks the first part of #2845:

  • introduces the agreed new name _≈?_ for (instances of) DecidableEquality, as an alias for the field name _≟_
  • importantly does no deprecations of the latter (the proliferations of warnings needed for such a change would be prohibitive)
  • continues to export the old name as public, but now uses it nowhere except to construct new Relation.Binary.Structures
  • but does most of the heavy lifting of [ breaking ] change fieldname _≟_ to _≈?_ in IsDecEquivalence #2952 in using the new name everywhere else
  • gives enough hint in the CHANGELOG as to what is to come

Further: (and this could form part of the husk of a now hollwed-out #2952 )

  • plumbs in, in commented out code, the path to v3.0 deprecation of _≟_
  • leaving only the actual fieldname change to make

Aim:

  • the hard part of reviewing has already been done (thanks @JacquesCarette !), so hopefully this can be merged without too much controversy
  • the v3.0 step in this cycle of renaming/deprecation should now be 'straightforward'
  • better to get this stage done for v2.4

Comments welcome!

@jamesmckinna jamesmckinna added this to the v2.4 milestone Apr 16, 2026
@jamesmckinna

Copy link
Copy Markdown
Collaborator Author

Gonna do @gallais 's trick of close and re-open to kick-start rechecking the various haskell failing versions?

@JacquesCarette

Copy link
Copy Markdown
Collaborator

187 files, yikes. I've put that on my next stdlib pass. I have otherwise caught up with my backlog.

@jamesmckinna

Copy link
Copy Markdown
Collaborator Author

187 files, yikes. I've put that on my next stdlib pass. I have otherwise caught up with my backlog.

No, you did the bulk of this already on #2952 this PR is based off that one but doesn't make the breaking change of fieldname...

@JacquesCarette

Copy link
Copy Markdown
Collaborator

Unfortunately github can't seem to see that, so is asking me to review all of them again. But now that I know, I might be able to figure out what exactly is new here.

@jamesmckinna

Copy link
Copy Markdown
Collaborator Author

Unfortunately github can't seem to see that, so is asking me to review all of them again. But now that I know, I might be able to figure out what exactly is new here.

Apologies. This doubtless down to my clumsy use of hit and GitHub. I'd had the thought that having a v2.4 version would get the worst of the use changes out of the way, (and that you'd already surveyed), and the rename+deprecate cycle proper can begin in the v3.x product line...


lookup : ∀ {counted n} → counted ⊕ n → ∀ x → Dec (x ∈ counted)
lookup {counted} _ x = Any.any? (_≟_ x) counted
lookup {counted} _ x = x ∈? counted

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There's a subtle issue with this change: in the definition of _∈?_, the needle is on the left of the _≟_/_≈?_, but the old version you're replacing here has the needle on the right of the _≟_. I think this is an OK change to make, and being more consistent with the rest of the library is a worthy goal, but this should be a change we're making deliberately

Comment thread src/Algebra/Construct/LexProduct.agda
Comment thread src/Data/Char/Properties.agda Outdated
@Taneb

Taneb commented May 6, 2026

Copy link
Copy Markdown
Member

Compile issue with new module Data.Nat.Bounded.Base, which uses the now deprecated names

@gallais

gallais commented May 6, 2026

Copy link
Copy Markdown
Member

I'll push a fix.

@JacquesCarette JacquesCarette added this pull request to the merge queue May 29, 2026
@github-merge-queue github-merge-queue Bot removed this pull request from the merge queue due to a conflict with the base branch May 29, 2026
@Taneb Taneb enabled auto-merge May 30, 2026 07:51
@Taneb Taneb added this pull request to the merge queue Jun 8, 2026
Merged via the queue into agda:master with commit 97731c5 Jun 8, 2026
13 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants