The following functions can't be defined at Init.Data.List.Basic, because they depend on Init.Util, and Init.Util depends on Init.Data.List.Basic.

def List.get! {α : Type u_1} [Inhabited α] (as : List α) (i : Nat) : α

Returns the i-th element in the list (zero-based).

If the index is out of bounds (i ≥ as.length), this function panics when executed, and returns default. See get? and getD for safer alternatives.

Equations

• (a :: tail).get! 0 = a
• (head :: as).get! n.succ = as.get! n
• x✝.get! x = panicWithPosWithDecl "Init.Data.List.BasicAux" "List.get!" 25 18 "invalid index"

def List.get? {α : Type u_1} (as : List α) (i : Nat) : Option α

Returns the i-th element in the list (zero-based).

If the index is out of bounds (i ≥ as.length), this function returns none. Also see get, getD and get!.

Equations

• (a :: tail).get? 0 = some a
• (head :: as).get? n.succ = as.get? n
• x✝.get? x = none

def List.getD {α : Type u_1} (as : List α) (i : Nat) (fallback : α) : α

Returns the i-th element in the list (zero-based).

If the index is out of bounds (i ≥ as.length), this function returns fallback. See also get? and get!.

Equations

• as.getD i fallback = (as.get? i).getD fallback

theorem List.ext {α : Type u_1} {l₁ : List α} {l₂ : List α} : (∀ (n : Nat), l₁.get? n = l₂.get? n) → l₁ = l₂

def List.head! {α : Type u_1} [Inhabited α] : List α → α

Returns the first element in the list.

If the list is empty, this function panics when executed, and returns default. See head and headD for safer alternatives.

Equations

• x.head! = match x with | [] => panicWithPosWithDecl "Init.Data.List.BasicAux" "List.head!" 62 12 "empty list" | a :: tail => a

def List.head? {α : Type u_1} : List α → Option α

Returns the first element in the list.

If the list is empty, this function returns none. Also see headD and head!.

Equations

• x.head? = match x with | [] => none | a :: tail => some a

def List.headD {α : Type u_1} (as : List α) (fallback : α) : α

Returns the first element in the list.

If the list is empty, this function returns fallback. Also see head? and head!.

Equations

• x✝.headD x = match x✝, x with | [], fallback => fallback | a :: tail, x => a

def List.head {α : Type u_1} (as : List α) : as ≠ [] → α

Returns the first element of a non-empty list.

Equations

• x✝.head x = match x✝, x with | a :: tail, x => a

def List.tail! {α : Type u_1} : List α → List α

Drops the first element of the list.

If the list is empty, this function panics when executed, and returns the empty list. See tail and tailD for safer alternatives.

Equations

• x.tail! = match x with | [] => panicWithPosWithDecl "Init.Data.List.BasicAux" "List.tail!" 98 13 "empty list" | head :: as => as

def List.tail? {α : Type u_1} : List α → Option (List α)

Drops the first element of the list.

If the list is empty, this function returns none. Also see tailD and tail!.

Equations

• x.tail? = match x with | [] => none | head :: as => some as

def List.tailD {α : Type u_1} (list : List α) (fallback : List α) : List α

Drops the first element of the list.

If the list is empty, this function returns fallback. Also see head? and head!.

Equations

• list.tailD fallback = match list with | [] => fallback | head :: tl => tl

def List.getLast {α : Type u_1} (as : List α) : as ≠ [] → α

Returns the last element of a non-empty list.

Equations

• [].getLast h = absurd ⋯ h
• [a].getLast x_2 = a
• (head :: b :: as).getLast x_2 = (b :: as).getLast ⋯

def List.getLast! {α : Type u_1} [Inhabited α] : List α → α

Returns the last element in the list.

If the list is empty, this function panics when executed, and returns default. See getLast and getLastD for safer alternatives.

Equations

• x.getLast! = match x with | [] => panicWithPosWithDecl "Init.Data.List.BasicAux" "List.getLast!" 137 13 "empty list" | a :: as => (a :: as).getLast ⋯

def List.getLast? {α : Type u_1} : List α → Option α

Returns the last element in the list.

If the list is empty, this function returns none. Also see getLastD and getLast!.

Equations

• x.getLast? = match x with | [] => none | a :: as => some ((a :: as).getLast ⋯)

def List.getLastD {α : Type u_1} (as : List α) (fallback : α) : α

Returns the last element in the list.

If the list is empty, this function returns fallback. Also see getLast? and getLast!.

Equations

• x✝.getLastD x = match x✝, x with | [], a₀ => a₀ | a :: as, x => (a :: as).getLast ⋯

def List.rotateLeft {α : Type u_1} (xs : List α) (n : optParam Nat 1) : List α

O(n). Rotates the elements of xs to the left such that the element at xs[i] rotates to xs[(i - n) % l.length].

• rotateLeft [1, 2, 3, 4, 5] 3 = [4, 5, 1, 2, 3]
• rotateLeft [1, 2, 3, 4, 5] 5 = [1, 2, 3, 4, 5]
• rotateLeft [1, 2, 3, 4, 5] = [2, 3, 4, 5, 1]

Equations

• xs.rotateLeft n = let len := xs.length; if len ≤ 1 then xs else let n := n % len; let b := List.take n xs; let e := List.drop n xs; e ++ b

def List.rotateRight {α : Type u_1} (xs : List α) (n : optParam Nat 1) : List α

O(n). Rotates the elements of xs to the right such that the element at xs[i] rotates to xs[(i + n) % l.length].

• rotateRight [1, 2, 3, 4, 5] 3 = [3, 4, 5, 1, 2]
• rotateRight [1, 2, 3, 4, 5] 5 = [1, 2, 3, 4, 5]
• rotateRight [1, 2, 3, 4, 5] = [5, 1, 2, 3, 4]

Equations

• xs.rotateRight n = let len := xs.length; if len ≤ 1 then xs else let n := len - n % len; let b := List.take n xs; let e := List.drop n xs; e ++ b

theorem List.get_append_left {α : Type u_1} {i : Nat} (as : List α) (bs : List α) (h : i < as.length) {h' : i < (as ++ bs).length} : (as ++ bs).get ⟨i, h'⟩ = as.get ⟨i, h⟩

theorem List.get_append_right {α : Type u_1} {i : Nat} (as : List α) (bs : List α) (h : ¬i < as.length) {h' : i < (as ++ bs).length} {h'' : i - as.length < bs.length} : (as ++ bs).get ⟨i, h'⟩ = bs.get ⟨i - as.length, h''⟩

theorem List.get_last {α : Type u_1} {a : α} {as : List α} {i : Fin (as ++ [a]).length} (h : ¬↑i < as.length) : (as ++ [a]).get i = a

theorem List.sizeOf_lt_of_mem {α : Type u_1} {a : α} [SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a < sizeOf as

def List.tacticSizeOf_list_dec : Lean.ParserDescr

This tactic, added to the decreasing_trivial toolbox, proves that sizeOf a < sizeOf as when a ∈ as, which is useful for well founded recursions over a nested inductive like inductive T | mk : List T → T.

Equations

• List.tacticSizeOf_list_dec = Lean.ParserDescr.node `List.tacticSizeOf_list_dec 1024 (Lean.ParserDescr.nonReservedSymbol "sizeOf_list_dec" false)

theorem List.append_cancel_left {α : Type u_1} {as : List α} {bs : List α} {cs : List α} (h : as ++ bs = as ++ cs) : bs = cs

theorem List.append_cancel_right {α : Type u_1} {as : List α} {bs : List α} {cs : List α} (h : as ++ bs = cs ++ bs) : as = cs

@[simp]

theorem List.append_cancel_left_eq {α : Type u_1} (as : List α) (bs : List α) (cs : List α) : (as ++ bs = as ++ cs) = (bs = cs)

@[simp]

theorem List.append_cancel_right_eq {α : Type u_1} (as : List α) (bs : List α) (cs : List α) : (as ++ bs = cs ++ bs) = (as = cs)

@[simp]

theorem List.sizeOf_get {α : Type u_1} [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as

theorem List.le_antisymm {α : Type u_1} [LT α] [s : Antisymm fun (x x_1 : α) => ¬x < x_1] {as : List α} {bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) : as = bs

instance List.instAntisymmLeOfNotLt {α : Type u_1} [LT α] [Antisymm fun (x x_1 : α) => ¬x < x_1] : Antisymm fun (x x_1 : List α) => x ≤ x_1

Equations

• List.instAntisymmLeOfNotLt = { antisymm := ⋯ }

@[implemented_by _private.Init.Data.List.BasicAux.0.List.mapMonoMImp]

def List.mapMonoM {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (as : List α) (f : α → m α) : m (List α)

Monomorphic List.mapM. The internal implementation uses pointer equality, and does not allocate a new list if the result of each f a is a pointer equal value a.

Equations

• [].mapMonoM f = pure []
• (a :: tail).mapMonoM f = do let __do_lift ← f a let __do_lift_1 ← tail.mapMonoM f pure (__do_lift :: __do_lift_1)

def List.mapMono {α : Type u_1} (as : List α) (f : α → α) : List α

Equations

• as.mapMono f = (as.mapMonoM f).run

@[inline]

def List.partitionM {m : Type → Type u_1} {α : Type} [Monad m] (p : α → m Bool) (l : List α) : m (List α × List α)

Monadic generalization of List.partition.

This uses Array.toList and which isn't imported by Init.Data.List.Basic.

def posOrNeg (x : Int) : Except String Bool :=
  if x > 0 then pure true
  else if x < 0 then pure false
  else throw "Zero is not positive or negative"

partitionM posOrNeg [-1, 2, 3] = Except.ok ([2, 3], [-1])
partitionM posOrNeg [0, 2, 3] = Except.error "Zero is not positive or negative"

Equations

• List.partitionM p l = List.partitionM.go p l #[] #[]

@[specialize #[]]

def List.partitionM.go {m : Type → Type u_1} {α : Type} [Monad m] (p : α → m Bool) : List α → Array α → Array α → m (List α × List α)

Auxiliary for partitionM: partitionM.go p l acc₁ acc₂ returns (acc₁.toList ++ left, acc₂.toList ++ right) if partitionM p l returns (left, right).

Equations

• List.partitionM.go p [] x✝ x = pure (x✝.toList, x.toList)
• List.partitionM.go p (x_3 :: xs) x✝ x = do let __do_lift ← p x_3 if __do_lift = true then List.partitionM.go p xs (x✝.push x_3) x else List.partitionM.go p xs x✝ (x.push x_3)

@[inline]

def List.partitionMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β ⊕ γ) (l : List α) : List β × List γ

Given a function f : α → β ⊕ γ, partitionMap f l maps the list by f whilst partitioning the result it into a pair of lists, List β × List γ, partitioning the .inl _ into the left list, and the .inr _ into the right List.

partitionMap (id : Nat ⊕ Nat → Nat ⊕ Nat) [inl 0, inr 1, inl 2] = ([0, 2], [1])

Equations

• List.partitionMap f l = List.partitionMap.go f l #[] #[]

@[specialize #[]]

def List.partitionMap.go {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β ⊕ γ) : List α → Array β → Array γ → List β × List γ

Auxiliary for partitionMap: partitionMap.go f l acc₁ acc₂ = (acc₁.toList ++ left, acc₂.toList ++ right) if partitionMap f l = (left, right).

Equations

• List.partitionMap.go f [] x✝ x = (x✝.toList, x.toList)
• List.partitionMap.go f (x_3 :: xs) x✝ x = match f x_3 with | Sum.inl a => List.partitionMap.go f xs (x✝.push a) x | Sum.inr b => List.partitionMap.go f xs x✝ (x.push b)