Non-empty list type.

Stream: Is there code for X?

[Wrenna Robson]

Do we have a type for non-empty lists, either inductively defined or defined as a subtype (analogous to PNat in some ways)?

[Shreyas Srinivas]

docs#NEList sorry I recall there being something of this sort. Maybe it was in the fxylang repository

[Shreyas Srinivas]

https://github.com/arthurpaulino/FxyLang/blob/master/FxyLang/Implementation/NEList.lean

[Bolton Bailey]

In mathlib: docs#FreeSemigroup (I guess this is not inductively defined, but its existence means we probably don't have anything else?)

[Wrenna Robson]

Horrible, I hate it!