Common.List.NonEmpty

A List with at least one member.

structure List.NonEmpty (α : Type u_1) : Type u_1

• head : α
• tail : List α

instance List.instCoeNonEmptyList {α : Type u_1} : Coe (List.NonEmpty α) (List α)

Equations

• List.instCoeNonEmptyList = { coe := fun (xs : List.NonEmpty α) => xs.head :: xs.tail }

instance List.instCoeDepListConsNonEmpty {α : Type u_1} {x : α} {xs : List α} : CoeDep (List α) (x :: xs) (List.NonEmpty α)

Equations

• List.instCoeDepListConsNonEmpty = { coe := { head := x, tail := xs } }

def List.NonEmpty.length {α : Type u_1} (xs : List.NonEmpty α) : ℕ

The length of a List.NonEmpty.

Equations

• List.NonEmpty.length xs = 1 + List.length xs.tail

theorem List.NonEmpty.length_self_eq_one_add_length_tail {α : Type u_1} (xs : List.NonEmpty α) : List.NonEmpty.length xs = 1 + List.length xs.tail

The length of a List.NonEmpty is always one plus the length of its tail.

@[inline, reducible]

abbrev List.NonEmpty.inBounds {α : Type u_1} (xs : List.NonEmpty α) (i : ℕ) : Prop

A proof that an index is within the bounds of the List.NonEmpty.

Equations

• List.NonEmpty.inBounds xs i = (i < List.NonEmpty.length xs)

def List.NonEmpty.get {α : Type u_1} (xs : List.NonEmpty α) (i : ℕ) (h : List.NonEmpty.inBounds xs i) : α

Retrieves the member of the List.NonEmpty at the specified index.

Equations

• List.NonEmpty.get xs x✝ x = match x✝, x with | 0, x => xs.head | Nat.succ n, h => let_fun this := (_ : n < List.length xs.tail); xs.tail[n]

def List.NonEmpty.get? {α : Type u_1} : List.NonEmpty α → ℕ → Option α

Variant of get that returns an Option α in the case of an invalid index.

Equations

• List.NonEmpty.get? x✝ x = match x✝, x with | xs, 0 => some xs.head | xs, Nat.succ n => List.get? xs.tail n

instance List.NonEmpty.instGetElemNonEmptyNatInBounds {α : Type u_1} : GetElem (List.NonEmpty α) ℕ α List.NonEmpty.inBounds

Type class instance for allowing direct indexing notation.

Equations

• List.NonEmpty.instGetElemNonEmptyNatInBounds = { getElem := List.NonEmpty.get }

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

Convert a List.NonEmpty into a plain List.

Equations

• List.NonEmpty.toList xs = xs.head :: xs.tail

def List.NonEmpty.last {α : Type u_1} : List.NonEmpty α → α

Retrieve the last member of the List.NonEmpty.

Equations

• List.NonEmpty.last { head := head, tail := [] } = head
• List.NonEmpty.last { head := head, tail := x_1 :: xs } = List.NonEmpty.last { head := x_1, tail := xs }