Skip to content

feat: nonempty list type#1607

Draft
fgdorais wants to merge 1 commit intomainfrom
list1
Draft

feat: nonempty list type#1607
fgdorais wants to merge 1 commit intomainfrom
list1

Conversation

@fgdorais
Copy link
Copy Markdown
Collaborator

@fgdorais fgdorais commented Jan 7, 2026

Experimental WIP.

@fgdorais fgdorais added the WIP work in progress label Jan 7, 2026
ghost pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jan 7, 2026
Update Batteries branch for testing leanprover-community/batteries#1607
5bf067d
@ghost ghost added the builds-mathlib label Jan 7, 2026
@ghost
Copy link
Copy Markdown

ghost commented Jan 7, 2026

Mathlib CI status (docs):

@414owen
Copy link
Copy Markdown

414owen commented Jan 11, 2026

Hi @fgdorais
There's probably a reason why this isn't so, but wouldn't a length-indexed list obviate the need for a nonempty list, and be more general?
NonEmpty a could be modelled as IList (succ n) a, for some n.
You'd equally be able to express "a list with at least two elements", etc.

I'm also wondering whether we're going to see Semigroup, Functor, Applicative, and Monad instances for this?

@fgdorais fgdorais added the on-hiatus This PR will not be merged soon but it may be reconsidered later if need arises. label Jan 31, 2026
@fgdorais
Copy link
Copy Markdown
Collaborator Author

fgdorais commented Jan 31, 2026

See also the alternative implementation at #1609

@fgdorais fgdorais mentioned this pull request Jan 31, 2026
Draft
@fgdorais fgdorais removed the WIP work in progress label Jan 31, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

builds-mathlib on-hiatus This PR will not be merged soon but it may be reconsidered later if need arises.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@fgdorais @414owen
⚡