Skip to content

feat: nonempty list type #1607

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Draft
fgdorais wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

feat: nonempty list type #1607

fgdorais wants to merge 1 commit into from

Conversation

@fgdorais
Copy link
Collaborator

@fgdorais fgdorais commented Jan 7, 2026

Experimental WIP.

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

ghost commented Jan 7, 2026

Mathlib CI status (docs):

@414owen
Copy link

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
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.

3 participants

@fgdorais @414owen