structure Data.List.NonEmpty (α : Type u) : Type u

A non-empty list. Stores head : α and tail : List α, ensuring at least one element.

Unlike { l : List α // l ≠ [] }, this representation provides $O(1)$ head access without proof elimination. The canonical form is: $$\text{NonEmpty}(\alpha) \cong \alpha \times \text{List}(\alpha)$$

• head : α

  The first element, accessible in $O(1)$.

• tail : List α

  The remaining elements (possibly empty).

@[implicit_reducible]

instance Data.List.instBEqNonEmpty {α✝ : Type u_1} [BEq α✝] : BEq (NonEmpty α✝)

Equations

• Data.List.instBEqNonEmpty = { beq := Data.List.instBEqNonEmpty.beq }

def Data.List.instBEqNonEmpty.beq {α✝ : Type u_1} [BEq α✝] : NonEmpty α✝ → NonEmpty α✝ → Bool

Equations

• Data.List.instBEqNonEmpty.beq { head := a, tail := a_1 } { head := b, tail := b_1 } = (a == b && a_1 == b_1)
• Data.List.instBEqNonEmpty.beq x✝¹ x✝ = false

def Data.List.instOrdNonEmpty.ord {α✝ : Type u_1} [Ord α✝] : NonEmpty α✝ → NonEmpty α✝ → Ordering

Equations

• Data.List.instOrdNonEmpty.ord { head := a, tail := a_1 } { head := b, tail := b_1 } = (compare a b).then ((compare a_1 b_1).then Ordering.eq)

@[implicit_reducible]

instance Data.List.instOrdNonEmpty {α✝ : Type u_1} [Ord α✝] : Ord (NonEmpty α✝)

Equations

• Data.List.instOrdNonEmpty = { compare := Data.List.instOrdNonEmpty.ord }

@[implicit_reducible]

instance Data.List.instReprNonEmpty {α✝ : Type u_1} [Repr α✝] : Repr (NonEmpty α✝)

Equations

• Data.List.instReprNonEmpty = { reprPrec := Data.List.instReprNonEmpty.repr }

def Data.List.instReprNonEmpty.repr {α✝ : Type u_1} [Repr α✝] : NonEmpty α✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.List.instHashableNonEmpty {α✝ : Type u_1} [Hashable α✝] : Hashable (NonEmpty α✝)

Equations

• Data.List.instHashableNonEmpty = { hash := Data.List.instHashableNonEmpty.hash }

def Data.List.instHashableNonEmpty.hash {α✝ : Type u_1} [Hashable α✝] : NonEmpty α✝ → UInt64

Equations

• Data.List.instHashableNonEmpty.hash { head := a, tail := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

@[inline]

def Data.List.NonEmpty.singleton {α : Type u_1} (x : α) : NonEmpty α

Construct a singleton non-empty list. $$\text{singleton}(x) = [x]$$

Equations

• Data.List.NonEmpty.singleton x = { head := x, tail := [] }

@[inline]

def Data.List.NonEmpty.cons {α : Type u_1} (x : α) (xs : NonEmpty α) : NonEmpty α

Construct from head and tail. $$\text{cons}(x, xs) = x :: xs$$

Equations

• Data.List.NonEmpty.cons x xs = { head := x, tail := xs.head :: xs.tail }

@[inline]

def Data.List.NonEmpty.toList {α : Type u_1} (ne : NonEmpty α) : List α

Convert to a standard List. Always non-empty. $$\text{toList}(x, xs) = x :: xs$$

Equations

• ne.toList = ne.head :: ne.tail

def Data.List.NonEmpty.last {α : Type u_1} (ne : NonEmpty α) : α

The last element. Total — no Option needed. For a non-empty list $[x_1, \ldots, x_n]$ where $n \geq 1$: $$\text{last}([x_1, \ldots, x_n]) = x_n$$

Runs in $O(n)$ time.

Equations

• ne.last = Data.List.NonEmpty.last.go ne.head ne.tail

def Data.List.NonEmpty.last.go {α : Type u_1} (x : α) : List α → α

Equations

• Data.List.NonEmpty.last.go x [] = x
• Data.List.NonEmpty.last.go x (y :: ys) = Data.List.NonEmpty.last.go y ys

def Data.List.NonEmpty.length {α : Type u_1} (ne : NonEmpty α) : { n : Nat // n ≥ 1 }

The length of a non-empty list, guaranteed $\geq 1$. $$|\text{NonEmpty}| = 1 + |\text{tail}|$$

Returns a subtype proving the result is at least 1.

Equations

• ne.length = ⟨1 + ne.tail.length, ⋯⟩

def Data.List.NonEmpty.append {α : Type u_1} (xs ys : NonEmpty α) : NonEmpty α

Append a non-empty list to another. Result is non-empty. $$[x_1, \ldots, x_m] \mathbin{+\!\!+} [y_1, \ldots, y_n] = [x_1, \ldots, x_m, y_1, \ldots, y_n]$$

Equations

• xs.append ys = { head := xs.head, tail := xs.tail ++ ys.toList }

@[implicit_reducible]

instance Data.List.NonEmpty.instAppend {α : Type u_1} : Append (NonEmpty α)

Equations

• Data.List.NonEmpty.instAppend = { append := Data.List.NonEmpty.append }

def Data.List.NonEmpty.map {α : Type u_1} {β : Type u_2} (f : α → β) (ne : NonEmpty α) : NonEmpty β

Map a function over every element. $$\text{map}(f, [x_1, \ldots, x_n]) = [f(x_1), \ldots, f(x_n)]$$

Equations

• Data.List.NonEmpty.map f ne = { head := f ne.head, tail := List.map f ne.tail }

def Data.List.NonEmpty.reverse {α : Type u_1} (ne : NonEmpty α) : NonEmpty α

Reverse the non-empty list. $$\text{reverse}([x_1, \ldots, x_n]) = [x_n, \ldots, x_1]$$

Equations

• ne.reverse = match h : ne.toList.reverse with | [] => absurd h ⋯ | x :: xs => { head := x, tail := xs }

def Data.List.NonEmpty.foldr {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (ne : NonEmpty α) : β

Right fold over the non-empty list. $$\text{foldr}(f, z, [x_1, \ldots, x_n]) = f(x_1, f(x_2, \ldots f(x_n, z)))$$

Equations

• Data.List.NonEmpty.foldr f init ne = f ne.head (List.foldr f init ne.tail)

def Data.List.NonEmpty.foldr1 {α : Type u_1} (f : α → α → α) (ne : NonEmpty α) : α

Right fold without an initial value (uses the last element). $$\text{foldr1}(f, [x_1, \ldots, x_n]) = f(x_1, f(x_2, \ldots f(x_{n-1}, x_n)))$$

Equations

• Data.List.NonEmpty.foldr1 f ne = Data.List.NonEmpty.foldr1.go f ne.head ne.tail

def Data.List.NonEmpty.foldr1.go {α : Type u_1} (f : α → α → α) (x : α) : List α → α

Equations

• Data.List.NonEmpty.foldr1.go f x [] = x
• Data.List.NonEmpty.foldr1.go f x (y :: ys) = f x (Data.List.NonEmpty.foldr1.go f y ys)

def Data.List.NonEmpty.foldl1 {α : Type u_1} (f : α → α → α) (ne : NonEmpty α) : α

Left fold without an initial value. $$\text{foldl1}(f, [x_1, \ldots, x_n]) = f(\ldots f(f(x_1, x_2), x_3) \ldots, x_n)$$

Equations

• Data.List.NonEmpty.foldl1 f ne = List.foldl f ne.head ne.tail

def Data.List.NonEmpty.fromList? {α : Type u_1} : List α → Option (NonEmpty α)

Construct from a list, if non-empty. Returns some iff the input list is non-nil.

Equations

• Data.List.NonEmpty.fromList? [] = none
• Data.List.NonEmpty.fromList? (y :: ys) = some { head := y, tail := ys }

def Data.List.NonEmpty.fromList {α : Type u_1} (l : List α) (h : l ≠ []) : NonEmpty α

Construct from a list with proof of non-emptiness.

Equations

• Data.List.NonEmpty.fromList (x :: xs) x_1 = { head := x, tail := xs }

theorem Data.List.NonEmpty.toList_ne_nil {α : Type u_1} (ne : NonEmpty α) : ne.toList ≠ []

Converting to a list always yields a non-nil list.

theorem Data.List.NonEmpty.reverse_length {α : Type u_1} (ne : NonEmpty α) : ne.reverse.toList.length = ne.toList.length

The length of a reversed non-empty list equals the original length.

theorem Data.List.NonEmpty.toList_length {α : Type u_1} (ne : NonEmpty α) : ne.toList.length = 1 + ne.tail.length

toList preserves length.

theorem Data.List.NonEmpty.map_length {α : Type u_1} {β : Type u_2} (f : α → β) (ne : NonEmpty α) : (map f ne).toList.length = ne.toList.length

map preserves length.

@[implicit_reducible]

instance Data.List.NonEmpty.instFunctor : Functor NonEmpty

Equations

• Data.List.NonEmpty.instFunctor = { map := fun {α β : Type ?u.10} => Data.List.NonEmpty.map }

@[implicit_reducible]

instance Data.List.NonEmpty.instPure : Pure NonEmpty

Equations

• Data.List.NonEmpty.instPure = { pure := fun {α : Type ?u.6} (x : α) => Data.List.NonEmpty.singleton x }

@[implicit_reducible]

instance Data.List.NonEmpty.instBind : Bind NonEmpty

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.List.NonEmpty.instMonad : Monad NonEmpty

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.List.NonEmpty.instToString {α : Type u_1} [ToString α] : ToString (NonEmpty α)

Equations

• Data.List.NonEmpty.instToString = { toString := fun (ne : Data.List.NonEmpty α) => toString ne.toList }