Skip to content

[ refactor ] rename constructors of Data.List.Base.InitLast and friends - #3090

Open
jamesmckinna wants to merge 1 commit into
agda:masterfrom
jamesmckinna:rename-InitLast
Open

[ refactor ] rename constructors of Data.List.Base.InitLast and friends#3090
jamesmckinna wants to merge 1 commit into
agda:masterfrom
jamesmckinna:rename-InitLast

Conversation

@jamesmckinna

@jamesmckinna jamesmckinna commented Jul 26, 2026

Copy link
Copy Markdown
Collaborator

Fixes #3089

Question: we typically are happy to overload [] as a constructor name, rather than here, where we might ought to also rename the InitLast constructor to ‵[]... but would that be Going Too Far?

UPDATED: now marked as blocking on #3089 until/unless we can agree what any convention/policy for naming here should actually be...!?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

[ refactor ] rename + deprecate Data.List.Base. _∷ʳ′_

1 participant