Documentation

Batteries.Data.List.Basic

New definitions #

source
def List.Subset {α : Type u_1} (l₁ : List α) (l₂ : List α) :
Prop

l₁ ⊆ l₂ means that every element of l₁ is also an element of l₂, ignoring multiplicity.

Equations
  • l₁.Subset l₂ = ∀ ⦃a : α⦄, a ∈ l₁ → a ∈ l₂
source
instance List.instHasSubset_batteries {α : Type u_1} :
HasSubset (List α)
Equations
  • List.instHasSubset_batteries = { Subset := List.Subset }
source
instance List.instDecidableRelSubsetOfDecidableEq_batteries {α : Type u_1} [DecidableEq α] :
DecidableRel Subset
Equations
source
def List.bagInter {α : Type u_1} [BEq α] :
List α → List α → List α

Computes the "bag intersection" of l₁ and l₂, that is, the collection of elements of l₁ which are also in l₂. As each element is identified, it is removed from l₂, so elements are counted with multiplicity.

Equations
  • [].bagInter x = []
  • x.bagInter [] = []
  • (a :: l₁).bagInter x = if List.elem a x = true then a :: l₁.bagInter (x.erase a) else l₁.bagInter x
source
def List.diff {α : Type u_1} [BEq α] :
List α → List α → List α

Computes the difference of l₁ and l₂, by removing each element in l₂ from l₁.

Equations
  • x.diff [] = x
  • x.diff (a :: l₂) = if List.elem a x = true then (x.erase a).diff l₂ else x.diff l₂
source
def List.tail {α : Type u_1} :
List α → List α

Get the tail of a nonempty list, or return [] for [].

Equations
  • x.tail = match x with | [] => [] | head :: as => as
source
@[simp]
theorem List.tail_nil {α : Type u_1} :
[].tail = []
source
@[simp]
theorem List.tail_cons {α : Type u_1} {a : α} {as : List α} :
(a :: as).tail = as
source
@[inline]
def List.next? {α : Type u_1} :
List α → Option (α × List α)

Get the head and tail of a list, if it is nonempty.

Equations
  • x.next? = match x with | [] => none | a :: l => some (a, l)
source
@[inline]
def List.mapIdx {α : Type u_1} {β : Type u_2} (f : Nat → α → β) (as : List α) :
List β

Given a function f : Nat → α → β and as : list α, as = [a₀, a₁, ...], returns the list [f 0 a₀, f 1 a₁, ...].

Equations
source
@[specialize #[]]
def List.mapIdx.go {α : Type u_1} {β : Type u_2} (f : Nat → α → β) :
List α → Array β → List β

Auxiliary for mapIdx: mapIdx.go [a₀, a₁, ...] acc = acc.toList ++ [f acc.size a₀, f (acc.size + 1) a₁, ...]

Equations
source
@[inline]
def List.mapIdxM {α : Type u_1} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (f : Nat → α → m β) :
m (List β)

Monadic variant of mapIdx.

Equations
source
@[specialize #[]]
def List.mapIdxM.go {α : Type u_1} {β : Type v} {m : Type v → Type w} [Monad m] (f : Nat → α → m β) :
List α → Array β → m (List β)

Auxiliary for mapIdxM: mapIdxM.go as f acc = acc.toList ++ [← f acc.size a₀, ← f (acc.size + 1) a₁, ...]

Equations
source
@[specialize #[]]
def List.after {α : Type u_1} (p : α → Bool) :
List α → List α

after p xs is the suffix of xs after the first element that satisfies p, not including that element.

after      (· == 1) [0, 1, 2, 3] = [2, 3]
drop_while (· != 1) [0, 1, 2, 3] = [1, 2, 3]
Equations
source
@[inline]
def List.findIdx {α : Type u_1} (p : α → Bool) (l : List α) :
Nat

Returns the index of the first element satisfying p, or the length of the list otherwise.

Equations
source
@[specialize #[]]
def List.findIdx.go {α : Type u_1} (p : α → Bool) :
List α → Nat → Nat

Auxiliary for findIdx: findIdx.go p l n = findIdx p l + n

Equations
source
def List.indexOf {α : Type u_1} [BEq α] (a : α) :
List α → Nat

Returns the index of the first element equal to a, or the length of the list otherwise.

Equations
source
@[deprecated List.eraseIdx]
def List.removeNth {α : Type u} :
List α → Nat → List α

Alias of List.eraseIdx.

O(i). eraseIdx l i removes the i'th element of the list l.

  • erase [a, b, c, d, e] 0 = [b, c, d, e]
  • erase [a, b, c, d, e] 1 = [a, c, d, e]
  • erase [a, b, c, d, e] 5 = [a, b, c, d, e]
Equations
source
@[deprecated List.eraseIdxTR]
def List.removeNthTR {α : Type u_1} (l : List α) (n : Nat) :
List α

Alias of List.eraseIdxTR.

Tail recursive version of List.eraseIdx.

Equations
source
@[deprecated List.eraseIdx_eq_eraseIdxTR]
theorem List.removeNth_eq_removeNthTR :
@List.eraseIdx = @List.eraseIdxTR

Alias of List.eraseIdx_eq_eraseIdxTR.

source
def List.replaceF {α : Type u_1} (f : α → Option α) :
List α → List α

Replaces the first element of the list for which f returns some with the returned value.

Equations
source
@[inline]
def List.replaceFTR {α : Type u_1} (f : α → Option α) (l : List α) :
List α

Tail-recursive version of replaceF.

Equations
source
@[specialize #[]]
def List.replaceFTR.go {α : Type u_1} (f : α → Option α) :
List α → Array α → List α

Auxiliary for replaceFTR: replaceFTR.go f xs acc = acc.toList ++ replaceF f xs.

Equations
source
@[csimp]
theorem List.replaceF_eq_replaceFTR :
@List.replaceF = @List.replaceFTR
source
theorem List.replaceF_eq_replaceFTR.go (α : Type u_1) (p : α → Option α) (acc : Array α) (xs : List α) :
List.replaceFTR.go p xs acc = acc.data ++ List.replaceF p xs
source
@[inline]
def List.union {α : Type u_1} [BEq α] (l₁ : List α) (l₂ : List α) :
List α

Constructs the union of two lists, by inserting the elements of l₁ in reverse order to l₂. As a result, l₂ will always be a suffix, but only the last occurrence of each element in l₁ will be retained (but order will otherwise be preserved).

Equations
source
instance List.instUnionOfBEq_batteries {α : Type u_1} [BEq α] :
Union (List α)
Equations
  • List.instUnionOfBEq_batteries = { union := List.union }
source
@[inline]
def List.inter {α : Type u_1} [BEq α] (l₁ : List α) (l₂ : List α) :
List α

Constructs the intersection of two lists, by filtering the elements of l₁ that are in l₂. Unlike bagInter this does not preserve multiplicity: [1, 1].inter [1] is [1, 1].

Equations
source
instance List.instInterOfBEq_batteries {α : Type u_1} [BEq α] :
Inter (List α)
Equations
  • List.instInterOfBEq_batteries = { inter := List.inter }
source
inductive List.Sublist {α : Type u_1} :
List α → List α → Prop

l₁ <+ l₂, or Sublist l₁ l₂, says that l₁ is a (non-contiguous) subsequence of l₂.

  • slnil: ∀ {α : Type u_1}, [].Sublist []

    the base case: [] is a sublist of []

  • cons: ∀ {α : Type u_1} {l₁ l₂ : List α} (a : α), l₁.Sublist l₂ → l₁.Sublist (a :: l₂)

    If l₁ is a subsequence of l₂, then it is also a subsequence of a :: l₂.

  • cons₂: ∀ {α : Type u_1} {l₁ l₂ : List α} (a : α), l₁.Sublist l₂ → (a :: l₁).Sublist (a :: l₂)

    If l₁ is a subsequence of l₂, then a :: l₁ is a subsequence of a :: l₂.

Instances For
source
def List.«term_<+_» :
Lean.TrailingParserDescr

l₁ <+ l₂, or Sublist l₁ l₂, says that l₁ is a (non-contiguous) subsequence of l₂.

Equations
source
def List.isSublist {α : Type u_1} [BEq α] :
List α → List α → Bool

True if the first list is a potentially non-contiguous sub-sequence of the second list.

Equations
  • [].isSublist x = true
  • x.isSublist [] = false
  • (hd₁ :: tl₁).isSublist (hd₂ :: tl₂) = if (hd₁ == hd₂) = true then tl₁.isSublist tl₂ else (hd₁ :: tl₁).isSublist tl₂
source
def List.splitAt {α : Type u_1} (n : Nat) (l : List α) :
List α × List α

Split a list at an index.

splitAt 2 [a, b, c] = ([a, b], [c])
Equations
source
def List.splitAt.go {α : Type u_1} (l : List α) :
List α → Nat → Array α → List α × List α

Auxiliary for splitAt: splitAt.go l n xs acc = (acc.toList ++ take n xs, drop n xs) if n < length xs, else (l, []).

Equations
source
def List.splitAtD {α : Type u_1} (n : Nat) (l : List α) (dflt : α) :
List α × List α

Split a list at an index. Ensures the left list always has the specified length by right padding with the provided default element.

splitAtD 2 [a, b, c] x = ([a, b], [c])
splitAtD 4 [a, b, c] x = ([a, b, c, x], [])
Equations
source
def List.splitAtD.go {α : Type u_1} (dflt : α) :
Nat → List α → Array α → List α × List α

Auxiliary for splitAtD: splitAtD.go dflt n l acc = (acc.toList ++ left, right) if splitAtD n l dflt = (left, right).

Equations
source
def List.splitOnP {α : Type u_1} (P : α → Bool) (l : List α) :
List (List α)

Split a list at every element satisfying a predicate. The separators are not in the result.

[1, 1, 2, 3, 2, 4, 4].splitOnP (· == 2) = [[1, 1], [3], [4, 4]]
Equations
source
def List.splitOnP.go {α : Type u_1} (P : α → Bool) :
List α → List α → List (List α)

Auxiliary for splitOnP: splitOnP.go xs acc = res' where res' is obtained from splitOnP P xs by prepending acc.reverse to the first element.

Equations
source
@[inline]
def List.splitOnPTR {α : Type u_1} (P : α → Bool) (l : List α) :
List (List α)

Tail recursive version of splitOnP.

Equations
source
@[specialize #[]]
def List.splitOnPTR.go {α : Type u_1} (P : α → Bool) :
List α → Array α → Array (List α) → List (List α)

Auxiliary for splitOnP: splitOnP.go xs acc r = r.toList ++ res' where res' is obtained from splitOnP P xs by prepending acc.toList to the first element.

Equations
source
@[csimp]
theorem List.splitOnP_eq_splitOnPTR :
@List.splitOnP = @List.splitOnPTR
source
@[inline]
def List.splitOn {α : Type u_1} [BEq α] (a : α) (as : List α) :
List (List α)

Split a list at every occurrence of a separator element. The separators are not in the result.

[1, 1, 2, 3, 2, 4, 4].splitOn 2 = [[1, 1], [3], [4, 4]]
Equations
source
def List.modifyNthTail {α : Type u_1} (f : List α → List α) :
Nat → List α → List α

Apply a function to the nth tail of l. Returns the input without using f if the index is larger than the length of the List.

modifyNthTail f 2 [a, b, c] = [a, b] ++ f [c]
Equations
source
@[inline]
def List.modifyHead {α : Type u_1} (f : α → α) :
List α → List α

Apply f to the head of the list, if it exists.

Equations
source
@[simp]
theorem List.modifyHead_nil {α : Type u_1} (f : α → α) :
List.modifyHead f [] = []
source
@[simp]
theorem List.modifyHead_cons {α : Type u_1} (a : α) (l : List α) (f : α → α) :
List.modifyHead f (a :: l) = f a :: l
source
def List.modifyNth {α : Type u_1} (f : α → α) :
Nat → List α → List α

Apply f to the nth element of the list, if it exists.

Equations
source
def List.modifyNthTR {α : Type u_1} (f : α → α) (n : Nat) (l : List α) :
List α

Tail-recursive version of modifyNth.

Equations
source
def List.modifyNthTR.go {α : Type u_1} (f : α → α) :
List α → Nat → Array α → List α

Auxiliary for modifyNthTR: modifyNthTR.go f l n acc = acc.toList ++ modifyNth f n l.

Equations
source
theorem List.modifyNthTR_go_eq :
∀ {α : Type u_1} {f : α → α} {acc : Array α} (l : List α) (n : Nat), List.modifyNthTR.go f l n acc = acc.data ++ List.modifyNth f n l
source
@[csimp]
theorem List.modifyNth_eq_modifyNthTR :
@List.modifyNth = @List.modifyNthTR
source
@[inline]
def List.modifyLast {α : Type u_1} (f : α → α) (l : List α) :
List α

Apply f to the last element of l, if it exists.

Equations
source
@[specialize #[]]
def List.modifyLast.go {α : Type u_1} (f : α → α) :
List α → Array α → List α

Auxiliary for modifyLast: modifyLast.go f l acc = acc.toList ++ modifyLast f l.

Equations
source
def List.insertNth {α : Type u_1} (n : Nat) (a : α) :
List α → List α

insertNth n a l inserts a into the list l after the first n elements of l

insertNth 2 1 [1, 2, 3, 4] = [1, 2, 1, 3, 4]
Equations
source
@[inline]
def List.insertNthTR {α : Type u_1} (n : Nat) (a : α) (l : List α) :
List α

Tail-recursive version of insertNth.

Equations
source
def List.insertNthTR.go {α : Type u_1} (a : α) :
Nat → List α → Array α → List α

Auxiliary for insertNthTR: insertNthTR.go a n l acc = acc.toList ++ insertNth n a l.

Equations
source
theorem List.insertNthTR_go_eq :
∀ {α : Type u_1} {a : α} {acc : Array α} (n : Nat) (l : List α), List.insertNthTR.go a n l acc = acc.data ++ List.insertNth n a l
source
@[csimp]
theorem List.insertNth_eq_insertNthTR :
@List.insertNth = @List.insertNthTR
source
@[simp]
theorem List.headD_eq_head? {α : Type u_1} (l : List α) (a : α) :
l.headD a = l.head?.getD a
source
def List.takeD {α : Type u_1} :
Nat → List α → α → List α

Take n elements from a list l. If l has less than n elements, append n - length l elements x.

Equations
source
@[simp]
theorem List.takeD_zero {α : Type u_1} (l : List α) (a : α) :
List.takeD 0 l a = []
source
@[simp]
theorem List.takeD_succ {α : Type u_1} {n : Nat} (l : List α) (a : α) :
List.takeD (n + 1) l a = l.head?.getD a :: List.takeD n l.tail a
source
@[simp]
theorem List.takeD_nil {α : Type u_1} (n : Nat) (a : α) :
List.takeD n [] a = List.replicate n a
source
def List.takeDTR {α : Type u_1} (n : Nat) (l : List α) (dflt : α) :
List α

Tail-recursive version of takeD.

Equations
source
def List.takeDTR.go {α : Type u_1} (dflt : α) :
Nat → List α → Array α → List α

Auxiliary for takeDTR: takeDTR.go dflt n l acc = acc.toList ++ takeD n l dflt.

Equations
source
theorem List.takeDTR_go_eq :
∀ {α : Type u_1} {dflt : α} {acc : Array α} (n : Nat) (l : List α), List.takeDTR.go dflt n l acc = acc.data ++ List.takeD n l dflt
source
@[csimp]
theorem List.takeD_eq_takeDTR :
@List.takeD = @List.takeDTR
source
def List.leftpad {α : Type u_1} (n : Nat) (a : α) (l : List α) :
List α

Pads l : List α with repeated occurrences of a : α until it is of length n. If l is initially larger than n, just return l.

Equations
source
@[inline]
def List.leftpadTR {α : Type u_1} (n : Nat) (a : α) (l : List α) :
List α

Optimized version of leftpad.

Equations
source
@[csimp]
theorem List.leftpad_eq_leftpadTR :
@List.leftpad = @List.leftpadTR
source
def List.scanl {α : Type u_1} {β : Type u_2} (f : α → β → α) (a : α) :
List β → List α

Fold a function f over the list from the left, returning the list of partial results.

scanl (+) 0 [1, 2, 3] = [0, 1, 3, 6]
Equations
source
@[inline]
def List.scanlTR {α : Type u_1} {β : Type u_2} (f : α → β → α) (a : α) (l : List β) :
List α

Tail-recursive version of scanl.

Equations
source
@[specialize #[]]
def List.scanlTR.go {α : Type u_1} {β : Type u_2} (f : α → β → α) :
List β → α → Array α → List α

Auxiliary for scanlTR: scanlTR.go f l a acc = acc.toList ++ scanl f a l.

Equations
source
theorem List.scanlTR_go_eq :
∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1 → α} {a : α} {acc : Array α} (l : List α_1), List.scanlTR.go f l a acc = acc.data ++ List.scanl f a l
source
@[csimp]
theorem List.scanl_eq_scanlTR :
@List.scanl = @List.scanlTR
source
def List.scanr {α : Type u_1} {β : Type u_2} (f : α → β → β) (b : β) (l : List α) :
List β

Fold a function f over the list from the right, returning the list of partial results.

scanr (+) 0 [1, 2, 3] = [6, 5, 3, 0]
Equations
  • List.scanr f b l = match List.foldr (fun (a : α) (x : β × List β) => match x with | (b', l') => (f a b', b' :: l')) (b, []) l with | (b', l') => b' :: l'
source
@[specialize #[]]
def List.foldlIdx {α : Sort u_1} {β : Type u_2} (f : Nat → α → β → α) (init : α) :
List β → optParam Nat 0 → α

Fold a list from left to right as with foldl, but the combining function also receives each element's index.

Equations
source
@[specialize #[]]
def List.foldrIdx {α : Type u_1} {β : Sort u_2} (f : Nat → α → β → β) (init : β) (l : List α) (start : optParam Nat 0) :
β

Fold a list from right to left as with foldr, but the combining function also receives each element's index.

Equations
source
@[inline]
def List.findIdxs {α : Type u_1} (p : α → Bool) (l : List α) :
List Nat

findIdxs p l is the list of indexes of elements of l that satisfy p.

Equations
source
@[inline]
def List.indexesValues {α : Type u_1} (p : α → Bool) (l : List α) :
List (Nat × α)

Returns the elements of l that satisfy p together with their indexes in l. The returned list is ordered by index.

Equations
source
@[inline]
def List.indexesOf {α : Type u_1} [BEq α] (a : α) :
List α → List Nat

indexesOf a l is the list of all indexes of a in l. For example:

indexesOf a [a, b, a, a] = [0, 2, 3]
Equations
source
def List.findIdx? {α : Type u_1} (p : α → Bool) :
List α → optParam Nat 0 → Option Nat

Return the index of the first occurrence of an element satisfying p.

Equations
source
@[inline]
def List.indexOf? {α : Type u_1} [BEq α] (a : α) :
List α → Option Nat

Return the index of the first occurrence of a in the list.

Equations
source
@[inline]
def List.lookmap {α : Type u_1} (f : α → Option α) (l : List α) :
List α

lookmap is a combination of lookup and filterMap. lookmap f l will apply f : α → Option α to each element of the list, replacing a → b at the first value a in the list such that f a = some b.

Equations
source
@[specialize #[]]
def List.lookmap.go {α : Type u_1} (f : α → Option α) :
List α → Array α → List α

Auxiliary for lookmap: lookmap.go f l acc = acc.toList ++ lookmap f l.

Equations
source
@[inline]
def List.countP {α : Type u_1} (p : α → Bool) (l : List α) :
Nat

countP p l is the number of elements of l that satisfy p.

Equations
source
@[specialize #[]]
def List.countP.go {α : Type u_1} (p : α → Bool) :
List α → Nat → Nat

Auxiliary for countP: countP.go p l acc = countP p l + acc.

Equations
source
@[inline]
def List.count {α : Type u_1} [BEq α] (a : α) :
List α → Nat

count a l is the number of occurrences of a in l.

Equations
source
def List.IsPrefix {α : Type u_1} (l₁ : List α) (l₂ : List α) :
Prop

IsPrefix l₁ l₂, or l₁ <+: l₂, means that l₁ is a prefix of l₂, that is, l₂ has the form l₁ ++ t for some t.

Equations
Instances For
source
def List.IsSuffix {α : Type u_1} (l₁ : List α) (l₂ : List α) :
Prop

IsSuffix l₁ l₂, or l₁ <:+ l₂, means that l₁ is a suffix of l₂, that is, l₂ has the form t ++ l₁ for some t.

Equations
Instances For
source
def List.IsInfix {α : Type u_1} (l₁ : List α) (l₂ : List α) :
Prop

IsInfix l₁ l₂, or l₁ <:+: l₂, means that l₁ is a contiguous substring of l₂, that is, l₂ has the form s ++ l₁ ++ t for some s, t.

Equations
Instances For
source
def List.«term_<+:_» :
Lean.TrailingParserDescr

IsPrefix l₁ l₂, or l₁ <+: l₂, means that l₁ is a prefix of l₂, that is, l₂ has the form l₁ ++ t for some t.

Equations
source
def List.«term_<:+_» :
Lean.TrailingParserDescr

IsSuffix l₁ l₂, or l₁ <:+ l₂, means that l₁ is a suffix of l₂, that is, l₂ has the form t ++ l₁ for some t.

Equations
source
def List.«term_<:+:_» :
Lean.TrailingParserDescr

IsInfix l₁ l₂, or l₁ <:+: l₂, means that l₁ is a contiguous substring of l₂, that is, l₂ has the form s ++ l₁ ++ t for some s, t.

Equations
source
def List.inits {α : Type u_1} :
List α → List (List α)

inits l is the list of initial segments of l.

inits [1, 2, 3] = [[], [1], [1, 2], [1, 2, 3]]
Equations
source
def List.initsTR {α : Type u_1} (l : List α) :
List (List α)

Tail-recursive version of inits.

Equations
source
@[csimp]
theorem List.inits_eq_initsTR :
@List.inits = @List.initsTR
source
def List.tails {α : Type u_1} :
List α → List (List α)

tails l is the list of terminal segments of l.

tails [1, 2, 3] = [[1, 2, 3], [2, 3], [3], []]
Equations
  • [].tails = [[]]
  • (head :: as).tails = (head :: as) :: as.tails
source
def List.tailsTR {α : Type u_1} (l : List α) :
List (List α)

Tail-recursive version of tails.

Equations
source
def List.tailsTR.go {α : Type u_1} (l : List α) (acc : Array (List α)) :
List (List α)

Auxiliary for tailsTR: tailsTR.go l acc = acc.toList ++ tails l.

Equations
source
@[csimp]
theorem List.tails_eq_tailsTR :
@List.tails = @List.tailsTR
source
def List.sublists' {α : Type u_1} (l : List α) :
List (List α)

sublists' l is the list of all (non-contiguous) sublists of l. It differs from sublists only in the order of appearance of the sublists; sublists' uses the first element of the list as the MSB, sublists uses the first element of the list as the LSB.

sublists' [1, 2, 3] = [[], [3], [2], [2, 3], [1], [1, 3], [1, 2], [1, 2, 3]]
Equations
source
@[implemented_by List.sublistsFast]
def List.sublists {α : Type u_1} (l : List α) :
List (List α)

sublists l is the list of all (non-contiguous) sublists of l; cf. sublists' for a different ordering.

sublists [1, 2, 3] = [[], [1], [2], [1, 2], [3], [1, 3], [2, 3], [1, 2, 3]]
Equations
source
def List.sublistsFast {α : Type u_1} (l : List α) :
List (List α)

A version of List.sublists that has faster runtime performance but worse kernel performance

Equations
  • One or more equations did not get rendered due to their size.
source
inductive List.Forall₂ {α : Type u_1} {β : Type u_2} (R : α → β → Prop) :
List α → List β → Prop

Forall₂ R l₁ l₂ means that l₁ and l₂ have the same length, and whenever a is the nth element of l₁, and b is the nth element of l₂, then R a b is satisfied.

Instances For
source
@[simp]
theorem List.forall₂_cons {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a : α} {b : β} {l₁ : List α} {l₂ : List β} :
List.Forall₂ R (a :: l₁) (b :: l₂) ↔ R a b ∧ List.Forall₂ R l₁ l₂
source
def List.all₂ {α : Type u_1} {β : Type u_2} (r : α → β → Bool) :
List α → List β → Bool

Check for all elements a, b, where a and b are the nth element of the first and second List respectively, that r a b = true.

Equations
source
@[simp]
theorem List.all₂_eq_true {α : Type u_1} {β : Type u_2} {r : α → β → Bool} (l₁ : List α) (l₂ : List β) :
List.all₂ r l₁ l₂ = true ↔ List.Forall₂ (fun (x : α) (x_1 : β) => r x x_1 = true) l₁ l₂
source
instance List.instDecidableForall₂ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} [(a : α) → (b : β) → Decidable (R a b)] (l₁ : List α) (l₂ : List β) :
Decidable (List.Forall₂ R l₁ l₂)
Equations
source
def List.transpose {α : Type u_1} (l : List (List α)) :
List (List α)

Transpose of a list of lists, treated as a matrix.

transpose [[1, 2], [3, 4], [5, 6]] = [[1, 3, 5], [2, 4, 6]]
Equations
  • l.transpose = (List.foldr List.transpose.go #[] l).toList
source
def List.transpose.pop {α : Type u_1} (old : List α) :
List α → Id (List α × List α)

pop : List α → StateM (List α) (List α) transforms the input list old by taking the head of the current state and pushing it on the head of old. If the state list is empty, then old is left unchanged.

Equations
source
def List.transpose.go {α : Type u_1} (l : List α) (acc : Array (List α)) :
Array (List α)

go : List α → Array (List α) → Array (List α) handles the insertion of a new list into all the lists in the array: go [a, b, c] #[l₁, l₂, l₃] = #[a::l₁, b::l₂, c::l₃]. If the new list is too short, the later lists are unchanged, and if it is too long the array is extended:

go [a] #[l₁, l₂, l₃] = #[a::l₁, l₂, l₃]
go [a, b, c, d] #[l₁, l₂, l₃] = #[a::l₁, b::l₂, c::l₃, [d]]
Equations
source
def List.sections {α : Type u_1} :
List (List α) → List (List α)

List of all sections through a list of lists. A section of [L₁, L₂, ..., Lₙ] is a list whose first element comes from L₁, whose second element comes from L₂, and so on.

Equations
  • [].sections = [[]]
  • (l :: L).sections = L.sections.bind fun (s : List α) => List.map (fun (a : α) => a :: s) l
source
def List.sectionsTR {α : Type u_1} (L : List (List α)) :
List (List α)

Optimized version of sections.

Equations
  • L.sectionsTR = bif L.any List.isEmpty then [] else (List.foldr List.sectionsTR.go #[[]] L).toList
source
def List.sectionsTR.go {α : Type u_1} (l : List α) (acc : Array (List α)) :
Array (List α)

go : List α → Array (List α) → Array (List α) inserts one list into the accumulated list of sections acc: go [a, b] #[l₁, l₂] = [a::l₁, b::l₁, a::l₂, b::l₂].

Equations
source
theorem List.sections_eq_nil_of_isEmpty {α : Type u_1} {L : List (List α)} :
L.any List.isEmpty = true → L.sections = []
source
@[csimp]
theorem List.sections_eq_sectionsTR :
@List.sections = @List.sectionsTR
source
def List.eraseP {α : Type u_1} (p : α → Bool) :
List α → List α

eraseP p l removes the first element of l satisfying the predicate p.

Equations
source
@[inline]
def List.erasePTR {α : Type u_1} (p : α → Bool) (l : List α) :
List α

Tail-recursive version of eraseP.

Equations
source
@[specialize #[]]
def List.erasePTR.go {α : Type u_1} (p : α → Bool) (l : List α) :
List α → Array α → List α

Auxiliary for erasePTR: erasePTR.go p l xs acc = acc.toList ++ eraseP p xs, unless xs does not contain any elements satisfying p, where it returns l.

Equations
source
@[csimp]
theorem List.eraseP_eq_erasePTR :
@List.eraseP = @List.erasePTR
source
theorem List.eraseP_eq_erasePTR.go (α : Type u_1) (p : α → Bool) (l : List α) (acc : Array α) (xs : List α) :
l = acc.data ++ xs → List.erasePTR.go p l xs acc = acc.data ++ List.eraseP p xs
source
def List.extractP {α : Type u_1} (p : α → Bool) (l : List α) :
Option α × List α

extractP p l returns a pair of an element a of l satisfying the predicate p, and l, with a removed. If there is no such element a it returns (none, l).

Equations
source
def List.extractP.go {α : Type u_1} (p : α → Bool) (l : List α) :
List α → Array α → Option α × List α

Auxiliary for extractP: extractP.go p l xs acc = (some a, acc.toList ++ out) if extractP p xs = (some a, out), and extractP.go p l xs acc = (none, l) if extractP p xs = (none, _).

Equations
source
def List.revzip {α : Type u_1} (l : List α) :
List (α × α)

revzip l returns a list of pairs of the elements of l paired with the elements of l in reverse order.

revzip [1, 2, 3, 4, 5] = [(1, 5), (2, 4), (3, 3), (4, 2), (5, 1)]
Equations
  • l.revzip = l.zip l.reverse
source
def List.product {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) :
List (α × β)

product l₁ l₂ is the list of pairs (a, b) where a ∈ l₁ and b ∈ l₂.

product [1, 2] [5, 6] = [(1, 5), (1, 6), (2, 5), (2, 6)]
Equations
source
def List.productTR {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) :
List (α × β)

Optimized version of product.

Equations
source
@[csimp]
theorem List.product_eq_productTR :
@List.product = @List.productTR
source
def List.sigma {α : Type u_1} {σ : α → Type u_2} (l₁ : List α) (l₂ : (a : α) → List (σ a)) :
List ((a : α) × σ a)

sigma l₁ l₂ is the list of dependent pairs (a, b) where a ∈ l₁ and b ∈ l₂ a.

sigma [1, 2] (λ_, [(5 : Nat), 6]) = [(1, 5), (1, 6), (2, 5), (2, 6)]
Equations
source
def List.sigmaTR {α : Type u_1} {σ : α → Type u_2} (l₁ : List α) (l₂ : (a : α) → List (σ a)) :
List ((a : α) × σ a)

Optimized version of sigma.

Equations
  • l₁.sigmaTR l₂ = (List.foldl (fun (acc : Array ((a : α) × σ a)) (a : α) => List.foldl (fun (acc : Array ((a : α) × σ a)) (b : σ a) => acc.push ⟨a, b⟩) acc (l₂ a)) #[] l₁).toList
source
@[csimp]
theorem List.sigma_eq_sigmaTR :
@List.sigma = @List.sigmaTR
source
def List.ofFn {α : Type u_1} {n : Nat} (f : Fin n → α) :
List α

ofFn f with f : fin n → α returns the list whose ith element is f i

ofFn f = [f 0, f 1, ... , f (n - 1)]
Equations
source
def List.ofFn.go {α : Type u_1} {n : Nat} (f : Fin n → α) (i : Nat) (j : Nat) (h : i + j = n) :
List α

Auxiliary for List.ofFn. ofFn.go f i j _ = [f j, ..., f (n - 1)].

Equations
source
@[inline]
def List.ofFnTR {α : Type u_1} {n : Nat} (f : Fin n → α) :
List α

Tail-recursive version of ofFn.

Equations
source
def List.ofFnTR.go {α : Type u_1} {n : Nat} (f : Fin n → α) (i : Nat) (h : i ≤ n) :
List α → List α

Auxiliary for List.ofFnTR. ofFnTR.go f i _ acc = f 0 :: ... :: f (i - 1) :: acc.

Equations
source
@[csimp]
theorem List.ofFn_eq_ofFnTR :
@List.ofFn = @List.ofFnTR
source
@[irreducible]
theorem List.ofFn_eq_ofFnTR.go (α : Type u_1) (n : Nat) (f : Fin n → α) (i : Nat) (j : Nat) (h : i + j = n) (h' : j ≤ n) :
List.ofFnTR.go f j h' (List.ofFn.go f i j h) = List.ofFn f
source
def List.ofFnNthVal {α : Type u_1} {n : Nat} (f : Fin n → α) (i : Nat) :
Option α

ofFnNthVal f i returns some (f i) if i < n and none otherwise.

Equations
source
def List.Disjoint {α : Type u_1} (l₁ : List α) (l₂ : List α) :
Prop

disjoint l₁ l₂ means that l₁ and l₂ have no elements in common.

Equations
  • l₁.Disjoint l₂ = ∀ ⦃a : α⦄, a ∈ l₁ → a ∈ l₂ → False
source
def List.takeWhile₂ {α : Type u_1} {β : Type u_2} (R : α → β → Bool) :
List α → List β → List α × List β

Returns the longest initial prefix of two lists such that they are pairwise related by R.

takeWhile₂ (· < ·) [1, 2, 4, 5] [5, 4, 3, 6] = ([1, 2], [5, 4])
Equations
source
@[inline]
def List.takeWhile₂TR {α : Type u_1} {β : Type u_2} (R : α → β → Bool) (as : List α) (bs : List β) :
List α × List β

Tail-recursive version of takeWhile₂.

Equations
source
@[specialize #[]]
def List.takeWhile₂TR.go {α : Type u_1} {β : Type u_2} (R : α → β → Bool) :
List α → List β → List α → List β → List α × List β

Auxiliary for takeWhile₂TR: takeWhile₂TR.go R as bs acca accb = (acca.reverse ++ as', acca.reverse ++ bs') if takeWhile₂ R as bs = (as', bs').

Equations
source
@[csimp]
theorem List.takeWhile₂_eq_takeWhile₂TR :
@List.takeWhile₂ = @List.takeWhile₂TR
source
@[irreducible]
theorem List.takeWhile₂_eq_takeWhile₂TR.go (α : Type u_2) (β : Type u_1) (R : α → β → Bool) (as : List α) (bs : List β) (acca : List α) (accb : List β) :
List.takeWhile₂TR.go R as bs acca accb = (acca.reverse ++ (List.takeWhile₂ R as bs).fst, accb.reverse ++ (List.takeWhile₂ R as bs).snd)
source
inductive List.Pairwise {α : Type u_1} (R : α → α → Prop) :
List α → Prop

Pairwise R l means that all the elements with earlier indexes are R-related to all the elements with later indexes.

Pairwise R [1, 2, 3] ↔ R 1 2 ∧ R 1 3 ∧ R 2 3

For example if R = (·≠·) then it asserts l has no duplicates, and if R = (·<·) then it asserts that l is (strictly) sorted.

Instances For
source
@[simp]
theorem List.pairwise_cons {α : Type u_1} {R : α → α → Prop} {a : α} {l : List α} :
List.Pairwise R (a :: l) ↔ (∀ (a' : α), a' ∈ l → R a a') ∧ List.Pairwise R l
source
instance List.instDecidablePairwise {α : Type u_1} {R : α → α → Prop} [DecidableRel R] (l : List α) :
Decidable (List.Pairwise R l)
Equations
  • One or more equations did not get rendered due to their size.
  • [].instDecidablePairwise = isTrue ⋯
source
def List.pwFilter {α : Type u_1} (R : α → α → Prop) [DecidableRel R] (l : List α) :
List α

pwFilter R l is a maximal sublist of l which is Pairwise R. pwFilter (·≠·) is the erase duplicates function (cf. eraseDup), and pwFilter (·<·) finds a maximal increasing subsequence in l. For example,

pwFilter (·<·) [0, 1, 5, 2, 6, 3, 4] = [0, 1, 2, 3, 4]
Equations
source
inductive List.Chain {α : Type u_1} (R : α → α → Prop) :
α → List α → Prop

Chain R a l means that R holds between adjacent elements of a::l.

Chain R a [b, c, d] ↔ R a b ∧ R b c ∧ R c d
  • nil: ∀ {α : Type u_1} {R : α → α → Prop} {a : α}, List.Chain R a []

    A chain of length 1 is trivially a chain.

  • cons: ∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α}, R a b → List.Chain R b l → List.Chain R a (b :: l)

    If a relates to b and b::l is a chain, then a :: b :: l is also a chain.

Instances For
source
def List.Chain' {α : Type u_1} (R : α → α → Prop) :
List α → Prop

Chain' R l means that R holds between adjacent elements of l.

Chain' R [a, b, c, d] ↔ R a b ∧ R b c ∧ R c d
Equations
Instances For
source
def List.Nodup {α : Type u_1} :
List α → Prop

Nodup l means that l has no duplicates, that is, any element appears at most once in the List. It is defined as Pairwise (≠).

Equations
Instances For
source
instance List.nodupDecidable {α : Type u_1} [DecidableEq α] (l : List α) :
Decidable l.Nodup
Equations
  • List.nodupDecidable = List.instDecidablePairwise
source
@[inline]
def List.eraseDup {α : Type u_1} [BEq α] :
List α → List α

eraseDup l removes duplicates from l (taking only the first occurrence). Defined as pwFilter (≠).

eraseDup [1, 0, 2, 2, 1] = [0, 2, 1]
Equations
source
def List.range' (start : Nat) (len : Nat) (step : optParam Nat 1) :
List Nat

range' start len step is the list of numbers [start, start+step, ..., start+(len-1)*step]. It is intended mainly for proving properties of range and iota.

Equations
source
@[inline]
def List.range'TR (s : Nat) (n : Nat) (step : optParam Nat 1) :
List Nat

Optimized version of range'.

Equations
source
def List.range'TR.go (step : optParam Nat 1) :
Nat → Nat → List Nat → List Nat

Auxiliary for range'TR: range'TR.go n e = [e-n, ..., e-1] ++ acc.

Equations
source
@[csimp]
theorem List.range'_eq_range'TR :
@List.range' = @List.range'TR
source
theorem List.range'_eq_range'TR.go (step : optParam Nat 1) (s : Nat) (n : Nat) (m : Nat) :
List.range'TR.go step n (s + step * n) (List.range' (s + step * n) m step) = List.range' s (n + m) step
source
@[inline]
def List.reduceOption {α : Type u_1} :
List (Option α) → List α

Drop nones from a list, and replace each remaining some a with a.

Equations
source
@[deprecated List.getLastD]
def List.ilast' {α : Type u_1} :
α → List α → α

ilast' x xs returns the last element of xs if xs is non-empty; it returns x otherwise. Use List.getLastD instead.

Equations
source
@[deprecated List.getLast?]
def List.last' {α : Type u_1} :
List α → Option α

last' xs returns the last element of xs if xs is non-empty; it returns none otherwise. Use List.getLast? instead

Equations
  • [].last' = none
  • [a].last' = some a
  • (head :: l).last' = l.last'
source
@[inline]
def List.rotate {α : Type u_1} (l : List α) (n : Nat) :
List α

rotate l n rotates the elements of l to the left by n

rotate [0, 1, 2, 3, 4, 5] 2 = [2, 3, 4, 5, 0, 1]
Equations
  • l.rotate n = match List.splitAt (n % l.length) l with | (l₁, l₂) => l₂ ++ l₁
source
def List.rotate' {α : Type u_1} :
List α → Nat → List α

rotate' is the same as rotate, but slower. Used for proofs about rotate

Equations
  • [].rotate' x = []
  • x.rotate' 0 = x
  • (a :: l).rotate' n.succ = (l ++ [a]).rotate' n
source
def List.mapDiagM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → α → m β) (l : List α) :
m (List β)

mapDiagM f l calls f on all elements in the upper triangular part of l × l. That is, for each e ∈ l, it will run f e e and then f e e' for each e' that appears after e in l.

mapDiagM f [1, 2, 3] =
  return [← f 1 1, ← f 1 2, ← f 1 3, ← f 2 2, ← f 2 3, ← f 3 3]
Equations
source
def List.mapDiagM.go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → α → m β) :
List α → Array β → m (List β)

Auxiliary for mapDiagM: mapDiagM.go as f acc = (acc.toList ++ ·) <$> mapDiagM f as

Equations
source
def List.forDiagM {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] (f : α → α → m PUnit) :
List α → m PUnit

forDiagM f l calls f on all elements in the upper triangular part of l × l. That is, for each e ∈ l, it will run f e e and then f e e' for each e' that appears after e in l.

forDiagM f [1, 2, 3] = do f 1 1; f 1 2; f 1 3; f 2 2; f 2 3; f 3 3
Equations
source
def List.getRest {α : Type u_1} [DecidableEq α] :
List α → List α → Option (List α)

getRest l l₁ returns some l₂ if l = l₁ ++ l₂. If l₁ is not a prefix of l, returns none

Equations
  • x.getRest [] = some x
  • [].getRest x = none
  • (x_2 :: l).getRest (y :: l₁) = if x_2 = y then l.getRest l₁ else none
source
def List.dropSlice {α : Type u_1} :
Nat → Nat → List α → List α

List.dropSlice n m xs removes a slice of length m at index n in list xs.

Equations
source
@[inline]
def List.dropSliceTR {α : Type u_1} (n : Nat) (m : Nat) (l : List α) :
List α

Optimized version of dropSlice.

Equations
source
def List.dropSliceTR.go {α : Type u_1} (l : List α) (m : Nat) :
List α → Nat → Array α → List α

Auxiliary for dropSliceTR: dropSliceTR.go l m xs n acc = acc.toList ++ dropSlice n m xs unless n ≥ length xs, in which case it is l.

Equations
source
theorem List.dropSlice_zero₂ {α : Type u_1} (n : Nat) (l : List α) :
List.dropSlice n 0 l = l
source
@[csimp]
theorem List.dropSlice_eq_dropSliceTR :
@List.dropSlice = @List.dropSliceTR
source
theorem List.dropSlice_eq_dropSliceTR.go (α : Type u_1) (l : List α) (m : Nat) (acc : Array α) (xs : List α) (n : Nat) :
l = acc.data ++ xs → List.dropSliceTR.go l m xs n acc = acc.data ++ List.dropSlice n (m + 1) xs
source
def List.zipWithLeft' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) :
List α → List β → List γ × List β

Left-biased version of List.zipWith. zipWithLeft' f as bs applies f to each pair of elements aᵢ ∈ as and bᵢ ∈ bs. If bs is shorter than as, f is applied to none for the remaining aᵢ. Returns the results of the f applications and the remaining bs.

zipWithLeft' prod.mk [1, 2] ['a'] = ([(1, some 'a'), (2, none)], [])
zipWithLeft' prod.mk [1] ['a', 'b'] = ([(1, some 'a')], ['b'])
Equations
source
@[inline]
def List.zipWithLeft'TR {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (as : List α) (bs : List β) :
List γ × List β

Tail-recursive version of zipWithLeft'.

Equations
source
def List.zipWithLeft'TR.go {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) :
List α → List β → Array γ → List γ × List β

Auxiliary for zipWithLeft'TR: zipWithLeft'TR.go l acc = acc.toList ++ zipWithLeft' l.

Equations
source
@[csimp]
theorem List.zipWithLeft'_eq_zipWithLeft'TR :
@List.zipWithLeft' = @List.zipWithLeft'TR
source
theorem List.zipWithLeft'_eq_zipWithLeft'TR.go (α : Type u_3) (β : Type u_2) (γ : Type u_1) (f : α → Option β → γ) (acc : Array γ) (as : List α) (bs : List β) :
List.zipWithLeft'TR.go f as bs acc = match List.zipWithLeft' f as bs with | (l, r) => (acc.toList ++ l, r)
source
@[inline]
def List.zipWithRight' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Option α → β → γ) (as : List α) (bs : List β) :
List γ × List α

Right-biased version of List.zipWith. zipWithRight' f as bs applies f to each pair of elements aᵢ ∈ as and bᵢ ∈ bs. If as is shorter than bs, f is applied to none for the remaining bᵢ. Returns the results of the f applications and the remaining as.

zipWithRight' prod.mk [1] ['a', 'b'] = ([(some 1, 'a'), (none, 'b')], [])
zipWithRight' prod.mk [1, 2] ['a'] = ([(some 1, 'a')], [2])
Equations
source
@[inline]
def List.zipLeft' {α : Type u_1} {β : Type u_2} :
List α → List β → List (α × Option β) × List β

Left-biased version of List.zip. zipLeft' as bs returns the list of pairs (aᵢ, bᵢ) for aᵢ ∈ as and bᵢ ∈ bs. If bs is shorter than as, the remaining aᵢ are paired with none. Also returns the remaining bs.

zipLeft' [1, 2] ['a'] = ([(1, some 'a'), (2, none)], [])
zipLeft' [1] ['a', 'b'] = ([(1, some 'a')], ['b'])
zipLeft' = zipWithLeft' prod.mk
Equations
source
@[inline]
def List.zipRight' {α : Type u_1} {β : Type u_2} :
List α → List β → List (Option α × β) × List α

Right-biased version of List.zip. zipRight' as bs returns the list of pairs (aᵢ, bᵢ) for aᵢ ∈ as and bᵢ ∈ bs. If as is shorter than bs, the remaining bᵢ are paired with none. Also returns the remaining as.

zipRight' [1] ['a', 'b'] = ([(some 1, 'a'), (none, 'b')], [])
zipRight' [1, 2] ['a'] = ([(some 1, 'a')], [2])
zipRight' = zipWithRight' prod.mk
Equations
source
def List.zipWithLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) :
List α → List β → List γ

Left-biased version of List.zipWith. zipWithLeft f as bs applies f to each pair aᵢ ∈ as and bᵢ ‌∈ bs‌∈ bs. If bs is shorter than as, f is applied to none for the remaining aᵢ.

zipWithLeft prod.mk [1, 2] ['a'] = [(1, some 'a'), (2, none)]
zipWithLeft prod.mk [1] ['a', 'b'] = [(1, some 'a')]
zipWithLeft f as bs = (zipWithLeft' f as bs).fst
Equations
source
@[inline]
def List.zipWithLeftTR {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (as : List α) (bs : List β) :
List γ

Tail-recursive version of zipWithLeft.

Equations
source
def List.zipWithLeftTR.go {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) :
List α → List β → Array γ → List γ

Auxiliary for zipWithLeftTR: zipWithLeftTR.go l acc = acc.toList ++ zipWithLeft l.

Equations
source
@[csimp]
theorem List.zipWithLeft_eq_zipWithLeftTR :
@List.zipWithLeft = @List.zipWithLeftTR
source
theorem List.zipWithLeft_eq_zipWithLeftTR.go (α : Type u_3) (β : Type u_2) (γ : Type u_1) (f : α → Option β → γ) (acc : Array γ) (as : List α) (bs : List β) :
List.zipWithLeftTR.go f as bs acc = acc.toList ++ List.zipWithLeft f as bs
source
@[inline]
def List.zipWithRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Option α → β → γ) (as : List α) (bs : List β) :
List γ

Right-biased version of List.zipWith. zipWithRight f as bs applies f to each pair aᵢ ∈ as and bᵢ ‌∈ bs‌∈ bs. If as is shorter than bs, f is applied to none for the remaining bᵢ.

zipWithRight prod.mk [1, 2] ['a'] = [(some 1, 'a')]
zipWithRight prod.mk [1] ['a', 'b'] = [(some 1, 'a'), (none, 'b')]
zipWithRight f as bs = (zipWithRight' f as bs).fst
Equations
source
@[inline]
def List.zipLeft {α : Type u_1} {β : Type u_2} :
List α → List β → List (α × Option β)

Left-biased version of List.zip. zipLeft as bs returns the list of pairs (aᵢ, bᵢ) for aᵢ ∈ as and bᵢ ∈ bs. If bs is shorter than as, the remaining aᵢ are paired with none.

zipLeft [1, 2] ['a'] = [(1, some 'a'), (2, none)]
zipLeft [1] ['a', 'b'] = [(1, some 'a')]
zipLeft = zipWithLeft prod.mk
Equations
source
@[inline]
def List.zipRight {α : Type u_1} {β : Type u_2} :
List α → List β → List (Option α × β)

Right-biased version of List.zip. zipRight as bs returns the list of pairs (aᵢ, bᵢ) for aᵢ ∈ as and bᵢ ∈ bs. If as is shorter than bs, the remaining bᵢ are paired with none.

zipRight [1, 2] ['a'] = [(some 1, 'a')]
zipRight [1] ['a', 'b'] = [(some 1, 'a'), (none, 'b')]
zipRight = zipWithRight prod.mk
Equations
source
@[inline]
def List.allSome {α : Type u_1} (l : List (Option α)) :
Option (List α)

If all elements of xs are some xᵢ, allSome xs returns the xᵢ. Otherwise it returns none.

allSome [some 1, some 2] = some [1, 2]
allSome [some 1, none  ] = none
Equations
source
def List.fillNones {α : Type u_1} :
List (Option α) → List α → List α

fillNones xs ys replaces the nones in xs with elements of ys. If there are not enough ys to replace all the nones, the remaining nones are dropped from xs.

fillNones [none, some 1, none, none] [2, 3] = [2, 1, 3]
Equations
  • [].fillNones x = []
  • (some a :: as).fillNones x = a :: as.fillNones x
  • (none :: as).fillNones [] = as.reduceOption
  • (none :: as).fillNones (a :: as') = a :: as.fillNones as'
source
@[inline]
def List.fillNonesTR {α : Type u_1} (as : List (Option α)) (as' : List α) :
List α

Tail-recursive version of fillNones.

Equations
source
def List.fillNonesTR.go {α : Type u_1} :
List (Option α) → List α → Array α → List α

Auxiliary for fillNonesTR: fillNonesTR.go as as' acc = acc.toList ++ fillNones as as'.

Equations
source
@[csimp]
theorem List.fillNones_eq_fillNonesTR :
@List.fillNones = @List.fillNonesTR
source
theorem List.fillNones_eq_fillNonesTR.go (α : Type u_1) (acc : Array α) (as : List (Option α)) (as' : List α) :
List.fillNonesTR.go as as' acc = acc.data ++ as.fillNones as'
source
def List.takeList {α : Type u_1} :
List α → List Nat → List (List α) × List α

takeList as ns extracts successive sublists from as. For ns = n₁ ... nₘ, it first takes the n₁ initial elements from as, then the next n₂ ones, etc. It returns the sublists of as -- one for each nᵢ -- and the remaining elements of as. If as does not have at least as many elements as the sum of the nᵢ, the corresponding sublists will have less than nᵢ elements.

takeList ['a', 'b', 'c', 'd', 'e'] [2, 1, 1] = ([['a', 'b'], ['c'], ['d']], ['e'])
takeList ['a', 'b'] [3, 1] = ([['a', 'b'], []], [])
Equations
  • x.takeList [] = ([], x)
  • x.takeList (n :: ns) = match List.splitAt n x with | (xs₁, xs₂) => match xs₂.takeList ns with | (xss, rest) => (xs₁ :: xss, rest)
source
@[inline]
def List.takeListTR {α : Type u_1} (xs : List α) (ns : List Nat) :
List (List α) × List α

Tail-recursive version of takeList.

Equations
source
def List.takeListTR.go {α : Type u_1} :
List Nat → List α → Array (List α) → List (List α) × List α

Auxiliary for takeListTR: takeListTR.go as as' acc = acc.toList ++ takeList as as'.

Equations
source
@[csimp]
theorem List.takeList_eq_takeListTR :
@List.takeList = @List.takeListTR
source
theorem List.takeList_eq_takeListTR.go (α : Type u_1) (acc : Array (List α)) (ns : List Nat) (xs : List α) :
List.takeListTR.go ns xs acc = match xs.takeList ns with | (l, r) => (acc.toList ++ l, r)
source
def List.toChunksAux {α : Type u_1} (n : Nat) :
List α → Nat → List α × List (List α)

Auxliary definition used to define toChunks. toChunksAux n xs i returns (xs.take i, (xs.drop i).toChunks (n+1)), that is, the first i elements of xs, and the remaining elements chunked into sublists of length n+1.

Equations
source
def List.toChunks {α : Type u_1} :
Nat → List α → List (List α)

xs.toChunks n splits the list into sublists of size at most n, such that (xs.toChunks n).join = xs.

[1, 2, 3, 4, 5, 6, 7, 8].toChunks 10 = [[1, 2, 3, 4, 5, 6, 7, 8]]
[1, 2, 3, 4, 5, 6, 7, 8].toChunks 3 = [[1, 2, 3], [4, 5, 6], [7, 8]]
[1, 2, 3, 4, 5, 6, 7, 8].toChunks 2 = [[1, 2], [3, 4], [5, 6], [7, 8]]
[1, 2, 3, 4, 5, 6, 7, 8].toChunks 0 = [[1, 2, 3, 4, 5, 6, 7, 8]]
Equations
source
def List.toChunks.go {α : Type u_1} (n : Nat) :
List α → Array α → Array (List α) → List (List α)

Auxliary definition used to define toChunks. toChunks.go xs acc₁ acc₂ pushes elements into acc₁ until it reaches size n, then it pushes the resulting list to acc₂ and continues until xs is exhausted.

Equations

We add some n-ary versions of List.zipWith for functions with more than two arguments. These can also be written in terms of List.zip or List.zipWith. For example, zipWith₃ f xs ys zs could also be written as zipWith id (zipWith f xs ys) zs or as (zip xs <| zip ys zs).map fun ⟨x, y, z⟩ => f x y z.

source
def List.zipWith₃ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β → γ → δ) :
List α → List β → List γ → List δ

Ternary version of List.zipWith.

Equations
source
def List.zipWith₄ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} (f : α → β → γ → δ → ε) :
List α → List β → List γ → List δ → List ε

Quaternary version of List.zipWith.

Equations
source
def List.zipWith₅ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ζ : Type u_6} (f : α → β → γ → δ → ε → ζ) :
List α → List β → List γ → List δ → List ε → List ζ

Quinary version of List.zipWith.

Equations
source
def List.mapWithPrefixSuffixAux {α : Type u_1} {β : Type u_2} (f : List α → α → List α → β) :
List α → List α → List β

An auxiliary function for List.mapWithPrefixSuffix.

Equations
source
def List.mapWithPrefixSuffix {α : Type u_1} {β : Type u_2} (f : List α → α → List α → β) (l : List α) :
List β

List.mapWithPrefixSuffix f l maps f across a list l. For each a ∈ l with l = pref ++ [a] ++ suff, a is mapped to f pref a suff. Example: if f : list Nat → Nat → list Nat → β, List.mapWithPrefixSuffix f [1, 2, 3] will produce the list [f [] 1 [2, 3], f [1] 2 [3], f [1, 2] 3 []].

Equations
source
def List.mapWithComplement {α : Type u_1} {β : Type u_2} (f : α → List α → β) :
List α → List β

List.mapWithComplement f l is a variant of List.mapWithPrefixSuffix that maps f across a list l. For each a ∈ l with l = pref ++ [a] ++ suff, a is mapped to f a (pref ++ suff), i.e., the list input to f is l with a removed. Example: if f : Nat → list Nat → β, List.mapWithComplement f [1, 2, 3] will produce the list [f 1 [2, 3], f 2 [1, 3], f 3 [1, 2]].

Equations
source
def List.traverse {F : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Applicative F] (f : α → F β) :
List α → F (List β)

Map each element of a List to an action, evaluate these actions in order, and collect the results.

Equations
source
inductive List.Perm {α : Type u_1} :
List α → List α → Prop

Perm l₁ l₂ or l₁ ~ l₂ asserts that l₁ and l₂ are permutations of each other. This is defined by induction using pairwise swaps.

  • nil: ∀ {α : Type u_1}, [].Perm []

    [] ~ []

  • cons: ∀ {α : Type u_1} (x : α) {l₁ l₂ : List α}, l₁.Perm l₂ → (x :: l₁).Perm (x :: l₂)

    l₁ ~ l₂ → x::l₁ ~ x::l₂

  • swap: ∀ {α : Type u_1} (x y : α) (l : List α), (y :: x :: l).Perm (x :: y :: l)

    x::y::l ~ y::x::l

  • trans: ∀ {α : Type u_1} {l₁ l₂ l₃ : List α}, l₁.Perm l₂ → l₂.Perm l₃ → l₁.Perm l₃

    Perm is transitive.

Instances For
source
def List.«term_~_» :
Lean.TrailingParserDescr

Perm l₁ l₂ or l₁ ~ l₂ asserts that l₁ and l₂ are permutations of each other. This is defined by induction using pairwise swaps.

Equations
source
def List.isPerm {α : Type u_1} [BEq α] :
List α → List α → Bool

O(|l₁| * |l₂|). Computes whether l₁ is a permutation of l₂. See isPerm_iff for a characterization in terms of List.Perm.

Equations
  • [].isPerm x = x.isEmpty
  • (a :: t).isPerm x = (x.contains a && t.isPerm (x.erase a))
source
def List.Subperm {α : Type u_1} (l₁ : List α) (l₂ : List α) :
Prop

Subperm l₁ l₂, denoted l₁ <+~ l₂, means that l₁ is a sublist of a permutation of l₂. This is an analogue of l₁ ⊆ l₂ which respects multiplicities of elements, and is used for the ≤ relation on multisets.

Equations
  • l₁.Subperm l₂ = ∃ (l : List α), l.Perm l₁ ∧ l.Sublist l₂
source
def List.«term_<+~_» :
Lean.TrailingParserDescr

Subperm l₁ l₂, denoted l₁ <+~ l₂, means that l₁ is a sublist of a permutation of l₂. This is an analogue of l₁ ⊆ l₂ which respects multiplicities of elements, and is used for the ≤ relation on multisets.

Equations
source
def List.isSubperm {α : Type u_1} [BEq α] (l₁ : List α) (l₂ : List α) :
Bool

O(|l₁| * (|l₁| + |l₂|)). Computes whether l₁ is a sublist of a permutation of l₂. See isSubperm_iff for a characterization in terms of List.Subperm.

Equations
source
def List.merge {α : Type u_1} (s : α → α → Bool) (l : List α) (r : List α) :
List α

O(|l| + |r|). Merge two lists using s as a switch.

Equations
source
@[irreducible]
def List.merge.loop {α : Type u_1} (s : α → α → Bool) :
List α → List α → List α → List α

Inner loop for List.merge. Tail recursive.

Equations