# Documentation

## Init.Data.List.BasicAux

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} [] :
List αNatα
Equations
Instances For
def List.get? {α : Type u_1} :
List αNat
Equations
Instances For
def List.getD {α : Type u_1} (as : List α) (idx : Nat) (a₀ : α) :
α
Equations
Instances For
def List.head! {α : Type u_1} [] :
List αα
Equations
• = match x with | [] => panicWithPosWithDecl "Init.Data.List.BasicAux" "List.head!" 32 12 "empty list" | a :: tail => a
Instances For
def List.head? {α : Type u_1} :
List α
Equations
• = match x with | [] => none | a :: tail => some a
Instances For
def List.headD {α : Type u_1} :
List ααα
Equations
• List.headD x✝ x = match x✝, x with | [], a₀ => a₀ | a :: tail, x => a
Instances For
def List.head {α : Type u_1} (as : List α) :
as []α
Equations
Instances For
def List.tail! {α : Type u_1} :
List αList α
Equations
• = match x with | [] => panicWithPosWithDecl "Init.Data.List.BasicAux" "List.tail!" 47 13 "empty list" | head :: as => as
Instances For
def List.tail? {α : Type u_1} :
List αOption (List α)
Equations
• = match x with | [] => none | head :: as => some as
Instances For
def List.tailD {α : Type u_1} :
List αList αList α
Equations
• List.tailD x✝ x = match x✝, x with | [], as₀ => as₀ | head :: as, x => as
Instances For
def List.getLast {α : Type u_1} (as : List α) :
as []α
Equations
Instances For
def List.getLast! {α : Type u_1} [] :
List αα
Equations
• One or more equations did not get rendered due to their size.
Instances For
def List.getLast? {α : Type u_1} :
List α
Equations
Instances For
def List.getLastD {α : Type u_1} :
List ααα
Equations
Instances For
def List.rotateLeft {α : Type u_1} (xs : List α) (n : ) :
List α
Equations
Instances For
def List.rotateRight {α : Type u_1} (xs : List α) (n : ) :
List α
Equations
Instances For
theorem List.get_append_left {α : Type u_1} {i : Nat} (as : List α) (bs : List α) (h : i < ) {h' : i < List.length (as ++ bs)} :
List.get (as ++ bs) { val := i, isLt := h' } = List.get as { val := i, isLt := h }
theorem List.get_append_right {α : Type u_1} {i : Nat} (as : List α) (bs : List α) (h : ¬i < ) {h' : i < List.length (as ++ bs)} {h'' : i - < } :
List.get (as ++ bs) { val := i, isLt := h' } = List.get bs { val := i - , isLt := h'' }
theorem List.get_last {α : Type u_1} {a : α} {as : List α} {i : Fin (List.length (as ++ [a]))} (h : ¬i < ) :
List.get (as ++ [a]) i = a
theorem List.sizeOf_lt_of_mem {α : Type u_1} {a : α} [] {as : List α} (h : a as) :
< sizeOf as

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
Instances For
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} [] (as : List α) (i : Fin ()) :
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.instAntisymmListLeInstLEList {α : Type u_1} [LT α] [Antisymm fun (x x_1 : α) => ¬x < x_1] :
Antisymm fun (x x_1 : List α) => x x_1
Equations
• List.instAntisymmListLeInstLEList = { antisymm := }
@[implemented_by _private.Init.Data.List.BasicAux.0.List.mapMonoMImp]
def List.mapMonoM {m : Type u_1 → Type u_2} {α : Type u_1} [] (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
Instances For
def List.mapMono {α : Type u_1} (as : List α) (f : αα) :
List α
Equations
Instances For
@[inline]
def List.partitionM {m : TypeType u_1} {α : Type} [] (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.

Equations
Instances For
@[specialize #[]]
def List.partitionM.go {m : TypeType u_1} {α : Type} [] (p : αm Bool) :
List α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
Instances For
@[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
Instances For
@[specialize #[]]
def List.partitionMap.go {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ γ) :
List αList β × List γ

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

Equations
Instances For