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 α] : List α → Nat → α

Equations

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

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

Equations

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

def List.getD {α : Type u_1} (as : List α) (idx : Nat) (a₀ : α) : α

Equations

• List.getD as idx a₀ = Option.getD (List.get? as idx) a₀

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

Equations

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

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

Equations

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

def List.headD {α : Type u_1} : List α → α → α

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def List.tailD {α : Type u_1} : List α → List α → List α

Equations

• List.tailD x✝ x = match x✝, x with | [], as₀ => as₀ | head :: as, x => as

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

Equations

• List.getLast [] h = absurd (_ : [] = []) h
• List.getLast [a] x_2 = a
• List.getLast (head :: b :: as) x_2 = List.getLast (b :: as) (_ : b :: as = [] → List.noConfusionType False (b :: as) [])

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

Equations

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

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

Equations

• List.getLast? x = match x with | [] => none | a :: as => some (List.getLast (a :: as) (_ : a :: as = [] → List.noConfusionType False (a :: as) []))

def List.getLastD {α : Type u_1} : List α → α → α

Equations

• List.getLastD x✝ x = match x✝, x with | [], a₀ => a₀ | a :: as, x => List.getLast (a :: as) (_ : a :: as = [] → List.noConfusionType False (a :: as) [])

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

Equations

• List.rotateLeft xs n = let len := List.length xs; 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 α

Equations

• List.rotateRight xs n = let len := List.length xs; 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 < List.length as) {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 < List.length as) {h' : i < List.length (as ++ bs)} {h'' : i - List.length as < List.length bs} : List.get (as ++ bs) { val := i, isLt := h' } = List.get bs { val := i - List.length as, isLt := h'' }

theorem List.get_last {α : Type u_1} {a : α} {as : List α} {i : Fin (List.length (as ++ [a]))} (h : ¬i.val < List.length as) : List.get (as ++ [a]) 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 (List.length as)) : sizeOf (List.get as 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.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 := (_ : ∀ {a b : List α}, a ≤ b → b ≤ a → a = b) }

@[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

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

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

Equations

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