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.

Alternative getters #

getD #

source

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

Returns the element at the provided index, counting from 0. Returns fallback if the index is out of bounds.

To return an Option depending on whether the index is in bounds, use as[i]?. To panic if the index is out of bounds, use as[i]!.

Examples:

["spring", "summer", "fall", "winter"].getD 2 "never" = "fall"
["spring", "summer", "fall", "winter"].getD 0 "never" = "spring"
["spring", "summer", "fall", "winter"].getD 4 "never" = "never"

Equations

as.getD i fallback = as[i]?.getD fallback

Instances For

source

@[simp]

theorem List.getD_nil {n : Nat} {α✝ : Type u_1} {d : α✝} :

[].getD n d = d

getLast! #

source

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

List α → α

Returns the last element in the list. Panics and returns default if the list is empty.

Safer alternatives include:

getLast?, which returns an Option,
getLastD, which takes a fallback value for empty lists, and
getLast, which requires a proof that the list is non-empty.

Examples:

["circle", "rectangle"].getLast! = "rectangle"
["circle"].getLast! = "circle"

Equations

[].getLast! = panicWithPosWithDecl "Init.Data.List.BasicAux" "List.getLast!" 59 13 "empty list"
(a :: as).getLast! = (a :: as).getLast ⋯

Instances For

Head and tail #

head! #

source

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

List α → α

Returns the first element in the list. If the list is empty, panics and returns default.

Safer alternatives include:

List.head, which requires a proof that the list is non-empty,
List.head?, which returns an Option, and
List.headD, which returns an explicitly-provided fallback value on empty lists.

Equations

[].head! = panicWithPosWithDecl "Init.Data.List.BasicAux" "List.head!" 75 12 "empty list"
(a :: as).head! = a

Instances For

tail! #

source

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

List α → List α

Drops the first element of a nonempty list, returning the tail. If the list is empty, this function panics when executed and returns the empty list.

Safer alternatives include

tail, which returns the empty list without panicking,
tail?, which returns an Option, and
tailD, which returns a fallback value when passed the empty list.

Examples:

["apple", "banana", "grape"].tail! = ["banana", "grape"]
["banana", "grape"].tail! = ["grape"]

Equations

[].tail! = panicWithPosWithDecl "Init.Data.List.BasicAux" "List.tail!" 94 13 "empty list"
(a :: as).tail! = as

Instances For

source

@[simp]

theorem List.tail!_cons {α : Type u_1} {a : α} {l : List α} :

(a :: l).tail! = l

partitionM #

source

@[inline]

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

m (List α × List α)

Returns a pair of lists that together contain all the elements of as. The first list contains those elements for which the monadic predicate p returns true, and the second contains those for which p returns false. The list's elements are examined in order, from left to right.

This is a monadic version of List.partition.

Example:

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"

#eval [-1, 2, 3].partitionM posOrNeg

Except.ok ([2, 3], [-1])

#eval [0, 2, 3].partitionM posOrNeg

Except.error "Zero is not positive or negative"

Equations

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

Instances For

partitionMap #

source

@[inline]

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

List β × List γ

Applies a function that returns a disjoint union to each element of a list, collecting the Sum.inl and Sum.inr results into separate lists.

Examples:

[0, 1, 2, 3].partitionMap (fun x => if x % 2 = 0 then .inl x else .inr x) = ([0, 2], [1, 3])
[0, 1, 2, 3].partitionMap (fun x => if x = 0 then .inl x else .inr x) = ([0], [1, 2, 3])

Equations

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

Instances For

mapMono #

This is a performance optimization for List.mapM that avoids allocating a new list when the result of each f a is a pointer equal value a.

For verification purposes, List.mapMono = List.map.

source

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

Applies a monadic function to each element of a list, returning the list of results. The function is monomorphic: it is required to return a value of the same type. The internal implementation uses pointer equality, and does not allocate a new list if the result of each function call is pointer-equal to its argument.

Equations

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

Instances For

source

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

List α

Applies a function to each element of a list, returning the list of results. The function is monomorphic: it is required to return a value of the same type. The internal implementation uses pointer equality, and does not allocate a new list if the result of each function call is pointer-equal to its argument.

For verification purposes, List.mapMono = List.map.

Equations

as.mapMono f = (as.mapMonoM fun (x : α) => pure (f x)).run

Instances For

Additional lemmas required for bootstrapping `Array`. #

source

@[simp]

theorem List.getElem_append_left {α : Type u_1} {i : Nat} {as bs : List α} (h : i < as.length) {h' : i < (as ++ bs).length} :

(as ++ bs)[i] = as[i]

source

@[simp]

theorem List.getElem_append_right {α : Type u_1} {as bs : List α} {i : Nat} (h₁ : as.length ≤ i) {h₂ : i < (as ++ bs).length} :

(as ++ bs)[i] = bs[i - as.length]

source

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

sizeOf a < sizeOf as

source

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)

Instances For

source

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

bs = cs

source

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

as = cs

source

@[simp]

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

(as ++ bs = as ++ cs) = (bs = cs)

source

@[simp]

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

(as ++ bs = cs ++ bs) = (as = cs)

source

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

sizeOf (as.get i) < sizeOf as

source

theorem List.not_lex_antisymm {α : Type u_1} [DecidableEq α] {r : α → α → Prop} [DecidableRel r] (antisymm : ∀ (x y : α), ¬r x y → ¬r y x → x = y) {as bs : List α} (h₁ : ¬Lex r bs as) (h₂ : ¬Lex r as bs) :

as = bs

source

theorem List.le_antisymm {α : Type u_1} [LT α] [i : Std.Antisymm fun (x1 x2 : α) => ¬x1 < x2] {as bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) :

as = bs

source

instance List.instAntisymmLeOfNotLt {α : Type u_1} [LT α] [s : Std.Antisymm fun (x1 x2 : α) => ¬x1 < x2] :

Std.Antisymm fun (x1 x2 : List α) => x1 ≤ x2

Alternative getters #

getD #

getLast! #

Head and tail #

head! #

tail! #

partitionM #

partitionMap #

mapMono #

Additional lemmas required for bootstrapping Array. #

Additional lemmas required for bootstrapping `Array`. #