Tail recursive implementations for definitions from core

ink

@[inline]

def List.setTR {α : Type u_1} (l : List α) (n : Nat) (a : α) : List α

Tail recursive version of erase.

Equations

• List.setTR l n a = List.setTR.go l a l n #[]

ink

def List.setTR.go {α : Type u_1} (l : List α) (a : α) : List α → Nat → Array α → List α

Auxiliary for setTR: setTR.go l a xs n acc = acc.toList ++ set xs a, unless n ≥ l.length≥ l.length in which case it returns l

Equations

• List.setTR.go l a [] x x = l
• List.setTR.go l a (head :: xs) 0 x = Array.toListAppend x (a :: xs)
• List.setTR.go l a (x_3 :: xs) (Nat.succ n) x = List.setTR.go l a xs n (Array.push x x_3)

ink

@[csimp]

theorem List.set_eq_setTR : @List.set = @List.setTR

ink

theorem List.set_eq_setTR.go (α : Type u_1) (l : List α) (a : α) (acc : Array α) (xs : List α) (n : Nat) : l = acc.data ++ xs → List.setTR.go l a xs n acc = acc.data ++ List.set xs n a

ink

@[inline]

def List.eraseTR {α : Type u_1} [inst : BEq α] (l : List α) (a : α) : List α

Tail recursive version of erase.

Equations

• List.eraseTR l a = List.eraseTR.go l a l #[]

ink

def List.eraseTR.go {α : Type u_1} [inst : BEq α] (l : List α) (a : α) : List α → Array α → List α

Auxiliary for eraseTR: eraseTR.go l a xs acc = acc.toList ++ erase xs a, unless a is not present in which case it returns l

Equations

• List.eraseTR.go l a [] x = l
• List.eraseTR.go l a (x_2 :: xs) x = bif x_2 == a then Array.toListAppend x xs else List.eraseTR.go l a xs (Array.push x x_2)

ink

@[csimp]

theorem List.erase_eq_eraseTR : @List.erase = @List.eraseTR

ink

@[inline]

def List.eraseIdxTR {α : Type u_1} (l : List α) (n : Nat) : List α

Tail recursive version of eraseIdx.

Equations

• List.eraseIdxTR l n = List.eraseIdxTR.go l l n #[]

ink

def List.eraseIdxTR.go {α : Type u_1} (l : List α) : List α → Nat → Array α → List α

Auxiliary for eraseIdxTR: eraseIdxTR.go l n xs acc = acc.toList ++ eraseIdx xs a, unless a is not present in which case it returns l

Equations

• List.eraseIdxTR.go l [] x x = l
• List.eraseIdxTR.go l (head :: xs) 0 x = Array.toListAppend x xs
• List.eraseIdxTR.go l (x_3 :: xs) (Nat.succ n) x = List.eraseIdxTR.go l xs n (Array.push x x_3)

ink

@[csimp]

theorem List.eraseIdx_eq_eraseIdxTR : @List.eraseIdx = @List.eraseIdxTR

ink

@[inline]

def List.bindTR {α : Type u_1} {β : Type u_2} (as : List α) (f : α → List β) : List β

Tail recursive version of bind.

Equations

• List.bindTR as f = List.bindTR.go f as #[]

ink

@[specialize #[]]

def List.bindTR.go {α : Type u_1} {β : Type u_2} (f : α → List β) : List α → Array β → List β

Auxiliary for bind: bind.go f as = acc.toList ++ bind f as

Equations

• List.bindTR.go f [] x = Array.toList x
• List.bindTR.go f (x_2 :: xs) x = List.bindTR.go f xs (x ++ f x_2)

ink

@[csimp]

theorem List.bind_eq_bindTR : @List.bind = @List.bindTR

ink

theorem List.bind_eq_bindTR.go (α : Type u_2) (β : Type u_1) (f : α → List β) (as : List α) (acc : Array β) : List.bindTR.go f as acc = acc.data ++ List.bind as f

ink

@[inline]

def List.joinTR {α : Type u_1} (l : List (List α)) : List α

Tail recursive version of join.

Equations

• List.joinTR l = List.bindTR l id

ink

@[csimp]

theorem List.join_eq_joinTR : @List.join = @List.joinTR

ink

@[inline]

def List.filterMapTR {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : List α) : List β

Tail recursive version of filterMap.

Equations

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

ink

@[specialize #[]]

def List.filterMapTR.go {α : Type u_1} {β : Type u_2} (f : α → Option β) : List α → Array β → List β

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

Equations

• List.filterMapTR.go f [] x = Array.toList x
• List.filterMapTR.go f (x_2 :: xs) x = match f x_2 with | none => List.filterMapTR.go f xs x | some b => List.filterMapTR.go f xs (Array.push x b)

ink

@[csimp]

theorem List.filterMap_eq_filterMapTR : @List.filterMap = @List.filterMapTR

ink

theorem List.filterMap_eq_filterMapTR.go (α : Type u_2) (β : Type u_1) (f : α → Option β) (as : List α) (acc : Array β) : List.filterMapTR.go f as acc = acc.data ++ List.filterMap f as

ink

@[inline]

def List.replaceTR {α : Type u_1} [inst : BEq α] (l : List α) (b : α) (c : α) : List α

Tail recursive version of replace.

Equations

• List.replaceTR l b c = List.replaceTR.go l b c l #[]

ink

@[specialize #[]]

def List.replaceTR.go {α : Type u_1} [inst : BEq α] (l : List α) (b : α) (c : α) : List α → Array α → List α

Auxiliary for replace: replace.go l b c xs acc = acc.toList ++ replace xs b c, unless b is not found in xs in which case it returns l.

Equations

• List.replaceTR.go l b c [] x = l
• List.replaceTR.go l b c (x_2 :: xs) x = bif x_2 == b then Array.toListAppend x (c :: xs) else List.replaceTR.go l b c xs (Array.push x x_2)

ink

@[csimp]

theorem List.replace_eq_replaceTR : @List.replace = @List.replaceTR

ink

@[inline]

def List.takeTR {α : Type u_1} (n : Nat) (l : List α) : List α

Tail recursive version of take.

Equations

• List.takeTR n l = List.takeTR.go l l n #[]

ink

@[specialize #[]]

def List.takeTR.go {α : Type u_1} (l : List α) : List α → Nat → Array α → List α

Auxiliary for take: take.go l xs n acc = acc.toList ++ take n xs, unless n ≥ xs.length≥ xs.length in which case it returns l.

Equations

• List.takeTR.go l [] x x = l
• List.takeTR.go l (head :: xs) 0 x = Array.toList x
• List.takeTR.go l (x_3 :: xs) (Nat.succ n) x = List.takeTR.go l xs n (Array.push x x_3)

ink

@[csimp]

theorem List.take_eq_takeTR : @List.take = @List.takeTR

ink

@[inline]

def List.takeWhileTR {α : Type u_1} (p : α → Bool) (l : List α) : List α

Tail recursive version of takeWhile.

Equations

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

ink

@[specialize #[]]

def List.takeWhileTR.go {α : Type u_1} (p : α → Bool) (l : List α) : List α → Array α → List α

Auxiliary for takeWhile: takeWhile.go p l xs acc = acc.toList ++ takeWhile p xs, unless no element satisfying p is found in xs in which case it returns l.

Equations

• List.takeWhileTR.go p l [] x = l
• List.takeWhileTR.go p l (x_2 :: xs) x = bif p x_2 then List.takeWhileTR.go p l xs (Array.push x x_2) else Array.toList x

ink

@[csimp]

theorem List.takeWhile_eq_takeWhileTR : @List.takeWhile = @List.takeWhileTR

ink

@[specialize #[]]

def List.foldrTR {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (l : List α) : β

Tail recursive version of foldr.

Equations

• List.foldrTR f init l = Array.foldr f init (List.toArray l) (Array.size (List.toArray l))

ink

@[csimp]

theorem List.foldr_eq_foldrTR : @List.foldr = @List.foldrTR

ink

@[inline]

def List.zipWithTR {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (as : List α) (bs : List β) : List γ

Tail recursive version of zipWith.

Equations

• List.zipWithTR f as bs = List.zipWithTR.go f as bs #[]

ink

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

Auxiliary for zipWith: zipWith.go f as bs acc = acc.toList ++ zipWith f as bs

Equations

• List.zipWithTR.go f (a :: as) (b :: bs) x = List.zipWithTR.go f as bs (Array.push x (f a b))
• List.zipWithTR.go f x x x = Array.toList x

ink

@[csimp]

theorem List.zipWith_eq_zipWithTR : @List.zipWith = @List.zipWithTR

ink

theorem List.zipWith_eq_zipWithTR.go (α : Type u_3) (β : Type u_2) (γ : Type u_1) (f : α → β → γ) (as : List α) (bs : List β) (acc : Array γ) : List.zipWithTR.go f as bs acc = acc.data ++ List.zipWith f as bs

ink

def List.unzipTR {α : Type u_1} {β : Type u_2} (l : List (α × β)) : List α × List β

Tail recursive version of unzip.

Equations

• List.unzipTR l = List.foldr (fun x x_1 => match x with | (a, b) => match x_1 with | (al, bl) => (a :: al, b :: bl)) ([], []) l

ink

@[csimp]

theorem List.unzip_eq_unzipTR : @List.unzip = @List.unzipTR

ink

def List.enumFromTR {α : Type u_1} (n : Nat) (l : List α) : List (Nat × α)

Tail recursive version of enumFrom.

Equations

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

ink

@[csimp]

theorem List.enumFrom_eq_enumFromTR : @List.enumFrom = @List.enumFromTR

ink

theorem List.enumFrom_eq_enumFromTR.go (α : Type u_1) (l : List α) (n : Nat) : let f := fun a x => match x with | (n, acc) => (n - 1, (n - 1, a) :: acc); List.foldr f (n + List.length l, []) l = (n, List.enumFrom n l)

ink

theorem List.replicateTR_loop_eq : ∀ {α : Type u_1} {a : α} {acc : List α} (n : Nat), List.replicateTR.loop a n acc = List.replicate n a ++ acc

ink

@[inline]

def List.dropLastTR {α : Type u_1} (l : List α) : List α

Tail recursive version of dropLast.

Equations

• List.dropLastTR l = Array.toList (Array.pop (List.toArray l))

ink

@[csimp]

theorem List.dropLast_eq_dropLastTR : @List.dropLast = @List.dropLastTR

ink

def List.intersperseTR {α : Type u_1} (sep : α) : List α → List α

Tail recursive version of intersperse.

Equations

• List.intersperseTR sep x = match x with | [] => [] | [x] => [x] | x :: y :: xs => x :: sep :: y :: List.foldr (fun a r => sep :: a :: r) [] xs

ink

@[csimp]

theorem List.intersperse_eq_intersperseTR : @List.intersperse = @List.intersperseTR

ink

def List.intercalateTR {α : Type u_1} (sep : List α) : List (List α) → List α

Tail recursive version of intercalate.

Equations

• List.intercalateTR sep x = match x with | [] => [] | [x] => x | x :: xs => List.intercalateTR.go (List.toArray sep) x xs #[]

ink

def List.intercalateTR.go {α : Type u_1} (sep : Array α) : List α → List (List α) → Array α → List α

Auxiliary for intercalateTR: intercalateTR.go sep x xs acc = acc.toList ++ intercalate sep.toList (x::xs)

Equations

• List.intercalateTR.go sep x [] x = Array.toListAppend x x
• List.intercalateTR.go sep x (y :: xs) x = List.intercalateTR.go sep y xs (x ++ x ++ sep)

ink

@[csimp]

theorem List.intercalate_eq_intercalateTR : @List.intercalate = @List.intercalateTR

ink

theorem List.intercalate_eq_intercalateTR.go (α : Type u_1) (sep : List α) {acc : Array α} {x : List α} (xs : List (List α)) : List.intercalateTR.go (List.toArray sep) x xs acc = acc.data ++ List.join (List.intersperse sep (x :: xs))

New definitions

ink

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

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

Equations

• List.Subset l₁ l₂ = ∀ ⦃a : α⦄, a ∈ l₁ → a ∈ l₂

ink

instance List.instHasSubsetList {α : Type u_1} : HasSubset (List α)

Equations

• List.instHasSubsetList = { Subset := List.Subset }

ink

instance List.decidableBEx {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (l : List α) : Decidable (∃ x, x ∈ l ∧ p x)

Equations

• One or more equations did not get rendered due to their size.
• List.decidableBEx p [] = isFalse (_ : (∃ x, x ∈ [] ∧ p x) → False)

ink

instance List.decidableBAll {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (l : List α) : Decidable ((x : α) → x ∈ l → p x)

Equations

• One or more equations did not get rendered due to their size.
• List.decidableBAll p [] = isTrue fun a a_1 => List.decidableBAll.match_1 (fun a a_2 => p a) a a_1

ink

def List.bagInter {α : Type u_1} [inst : 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

• List.bagInter [] x = []
• List.bagInter x [] = []
• List.bagInter (a :: l₁) x = if List.elem a x = true then a :: List.bagInter l₁ (List.erase x a) else List.bagInter l₁ x

ink

def List.diff {α : Type u_1} [inst : BEq α] : List α → List α → List α

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

Equations

• List.diff x [] = x
• List.diff x (a :: l₂) = if List.elem a x = true then List.diff (List.erase x a) l₂ else List.diff x l₂

ink

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

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

Equations

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

ink

@[simp]

theorem List.tail_nil {α : Type u_1} : List.tail [] = []

ink

@[simp]

theorem List.tail_cons {α : Type u_1} {a : α} {as : List α} : List.tail (a :: as) = as

ink

@[inline]

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

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

Equations

• List.next? x = match x with | [] => none | a :: l => some (a, l)

ink

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

• List.mapIdx f as = List.mapIdx.go f as #[]

ink

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

• List.mapIdx.go f [] x = Array.toList x
• List.mapIdx.go f (x_2 :: xs) x = List.mapIdx.go f xs (Array.push x (f (Array.size x) x_2))

ink

@[inline]

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

Monadic variant of mapIdx.

Equations

• List.mapIdxM as f = List.mapIdxM.go f as #[]

ink

@[specialize #[]]

def List.mapIdxM.go {α : Type u_1} {β : Type v} {m : Type v → Type w} [inst : 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₁, ...]← f acc.size a₀, ← f (acc.size + 1) a₁, ...]← f (acc.size + 1) a₁, ...]

Equations

• List.mapIdxM.go f [] x = pure (Array.toList x)
• List.mapIdxM.go f (x_2 :: xs) x = do let __do_lift ← f (Array.size x) x_2 List.mapIdxM.go f xs (Array.push x __do_lift)

ink

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

• List.after p [] = []
• List.after p (x_1 :: xs) = bif p x_1 then xs else List.after p xs

ink

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

• List.findIdx p l = List.findIdx.go p l 0

ink

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

• List.findIdx.go p [] x = x
• List.findIdx.go p (a :: l) x = bif p a then x else List.findIdx.go p l (x + 1)

ink

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

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

Equations

• List.indexOf a = List.findIdx fun x => a == x

ink

def List.removeNth {α : Type u_1} : List α → Nat → List α

Removes the nth element of l, or the original list if n is out of bounds.

Equations

• List.removeNth [] x = []
• List.removeNth (head :: xs) 0 = xs
• List.removeNth (x_2 :: xs) (Nat.succ i) = x_2 :: List.removeNth xs i

ink

@[inline]

def List.removeNthTR {α : Type u_1} (l : List α) (n : Nat) : List α

Tail recursive version of removeNth.

Equations

• List.removeNthTR l n = List.removeNthTR.go l l n #[]

ink

def List.removeNthTR.go {α : Type u_1} (l : List α) : List α → Nat → Array α → List α

Auxiliary for removeNthTR: removeNthTR.go l xs n acc = acc.toList ++ removeNth xs n if n < length xs, else l.

Equations

• List.removeNthTR.go l [] x x = l
• List.removeNthTR.go l (head :: xs) 0 x = Array.toListAppend x xs
• List.removeNthTR.go l (x_3 :: xs) (Nat.succ n) x = List.removeNthTR.go l xs n (Array.push x x_3)

ink

@[csimp]

theorem List.removeNth_eq_removeNthTR : @List.removeNth = @List.removeNthTR

ink

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

• List.replaceF f [] = []
• List.replaceF f (x_1 :: xs) = match f x_1 with | none => x_1 :: List.replaceF f xs | some a => a :: xs

ink

@[inline]

def List.replaceFTR {α : Type u_1} (f : α → Option α) (l : List α) : List α

Tail recursive version of replaceF.

Equations

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

ink

def List.replaceFTR.go {α : Type u_1} (f : α → Option α) (l : List α) : List α → Array α → List α

Auxiliary for replaceFTR: replaceFTR.go f l xs acc = acc.toList ++ replaceF f xs if f returns some, else l.

Equations

• List.replaceFTR.go f l [] x = l
• List.replaceFTR.go f l (x_2 :: xs) x = match f x_2 with | none => List.replaceFTR.go f l xs (Array.push x x_2) | some a => Array.toListAppend x (a :: xs)

ink

@[csimp]

theorem List.replaceF_eq_replaceFTR : @List.replaceF = @List.replaceFTR

ink

@[inline]

def List.insert {α : Type u_1} [inst : DecidableEq α] (a : α) (l : List α) : List α

Inserts an element into a list without duplication.

Equations

• List.insert a l = if a ∈ l then l else a :: l

ink

@[inline]

def List.union {α : Type u_1} [inst : DecidableEq α] (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

• List.union l₁ l₂ = List.foldr List.insert l₂ l₁

ink

instance List.instUnionList {α : Type u_1} [inst : DecidableEq α] : Union (List α)

Equations

• List.instUnionList = { union := List.union }

ink

@[inline]

def List.inter {α : Type u_1} [inst : DecidableEq α] (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

• List.inter l₁ l₂ = List.filter (fun x => decide (x ∈ l₂)) l₁

ink

instance List.instInterList {α : Type u_1} [inst : DecidableEq α] : Inter (List α)

Equations

• List.instInterList = { inter := List.inter }

ink

inductive List.Sublist {α : Type u_1} : List α → List α → Prop

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

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

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

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

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

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

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

ink

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

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

Equations

• List.«term_<+_» = Lean.ParserDescr.trailingNode `List.term_<+_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <+ ") (Lean.ParserDescr.cat `term 51))

ink

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

• List.splitAt n l = List.splitAt.go l l n #[]

ink

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

• List.splitAt.go l [] x x = (l, [])
• List.splitAt.go l (x_3 :: xs) (Nat.succ n) x = List.splitAt.go l xs n (Array.push x x_3)
• List.splitAt.go l x x x = (Array.toList x, x)

ink

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

• List.splitAtD n l dflt = List.splitAtD.go dflt n l #[]

ink

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

• List.splitAtD.go dflt (Nat.succ n) (x_3 :: xs) x = List.splitAtD.go dflt n xs (Array.push x x_3)
• List.splitAtD.go dflt 0 x x = (Array.toList x, x)
• List.splitAtD.go dflt x [] x = (Array.toListAppend x (List.replicate x dflt), [])

ink

@[inline]

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

• List.splitOnP P l = List.splitOnP.go P l #[] #[]

ink

@[specialize #[]]

def List.splitOnP.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

• List.splitOnP.go P [] x x = Array.toListAppend x [Array.toList x]
• List.splitOnP.go P (h :: t) x x = bif P h then List.splitOnP.go P t #[] (Array.push x (Array.toList x)) else List.splitOnP.go P t (Array.push x h) x

ink

@[inline]

def List.splitOn {α : Type u_1} [inst : 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

• List.splitOn a as = List.splitOnP (fun x => x == a) as

ink

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

• List.modifyNthTail f 0 x = f x
• List.modifyNthTail f (Nat.succ n) [] = []
• List.modifyNthTail f (Nat.succ n) (a :: l) = a :: List.modifyNthTail f n l

ink

@[inline]

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

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

Equations

• List.modifyHead f x = match x with | [] => [] | a :: l => f a :: l

ink

def List.modifyNth {α : Type u_1} (f : α → α) : Nat → List α → List α

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

Equations

• List.modifyNth f = List.modifyNthTail (List.modifyHead f)

ink

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

Tail-recursive version of modifyNth.

Equations

• List.modifyNthTR f n l = List.modifyNthTR.go f l n #[]

ink

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

• List.modifyNthTR.go f [] x x = Array.toList x
• List.modifyNthTR.go f (head :: xs) 0 x = Array.toListAppend x (f head :: xs)
• List.modifyNthTR.go f (x_3 :: xs) (Nat.succ n) x = List.modifyNthTR.go f xs n (Array.push x x_3)

ink

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

ink

@[csimp]

theorem List.modifyNth_eq_modifyNthTR : @List.modifyNth = @List.modifyNthTR

ink

@[inline]

def List.modifyLast {α : Type u_1} (f : α → α) (l : List α) : List α

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

Equations

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

ink

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

• List.modifyLast.go f [] x = []
• List.modifyLast.go f [x_2] x = Array.toListAppend x [f x_2]
• List.modifyLast.go f (x_2 :: xs) x = List.modifyLast.go f xs (Array.push x x_2)

ink

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

• List.insertNth n a = List.modifyNthTail (List.cons a) n

ink

@[inline]

def List.insertNthTR {α : Type u_1} (n : Nat) (a : α) (l : List α) : List α

Tail-recursive version of insertNth.

Equations

• List.insertNthTR n a l = List.insertNthTR.go a n l #[]

ink

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

• List.insertNthTR.go a 0 x x = Array.toListAppend x (a :: x)
• List.insertNthTR.go a x [] x = Array.toList x
• List.insertNthTR.go a (Nat.succ n) (a_1 :: l) x = List.insertNthTR.go a n l (Array.push x a_1)

ink

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

ink

@[csimp]

theorem List.insertNth_eq_insertNthTR : @List.insertNth = @List.insertNthTR

ink

@[simp]

theorem List.headD_eq_head? {α : Type u_1} (l : List α) (a : α) : List.headD l a = Option.getD (List.head? l) a

ink

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

• List.takeD 0 x x = []
• List.takeD (Nat.succ n) x x = List.headD x x :: List.takeD n (List.tail x) x

ink

@[simp]

theorem List.takeD_zero {α : Type u_1} (l : List α) (a : α) : List.takeD 0 l a = []

ink

@[simp]

theorem List.takeD_succ {α : Type u_1} {n : Nat} (l : List α) (a : α) : List.takeD (n + 1) l a = Option.getD (List.head? l) a :: List.takeD n (List.tail l) a

ink

@[simp]

theorem List.takeD_nil {α : Type u_1} (n : Nat) (a : α) : List.takeD n [] a = List.replicate n a

ink

def List.takeDTR {α : Type u_1} (n : Nat) (l : List α) (dflt : α) : List α

Tail-recursive version of takeD.

Equations

• List.takeDTR n l dflt = List.takeDTR.go dflt n l #[]

ink

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

• List.takeDTR.go dflt (Nat.succ n) (x_3 :: xs) x = List.takeDTR.go dflt n xs (Array.push x x_3)
• List.takeDTR.go dflt 0 x x = Array.toList x
• List.takeDTR.go dflt x [] x = Array.toListAppend x (List.replicate x dflt)

ink

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

ink

@[csimp]

theorem List.takeD_eq_takeDTR : @List.takeD = @List.takeDTR

ink

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

• List.leftpad n a l = List.replicate (n - List.length l) a ++ l

ink

@[inline]

def List.leftpadTR {α : Type u_1} (n : Nat) (a : α) (l : List α) : List α

Optimized version of leftpad.

Equations

• List.leftpadTR n a l = List.replicateTR.loop a (n - List.length l) l

ink

@[csimp]

theorem List.leftpad_eq_leftpadTR : @List.leftpad = @List.leftpadTR

ink

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

• List.scanl f a [] = [a]
• List.scanl f a (x_1 :: xs) = a :: List.scanl f (f a x_1) xs

ink

@[inline]

def List.scanlTR {α : Type u_1} {β : Type u_2} (f : α → β → α) (a : α) (l : List β) : List α

Tail-recursive version of scanl.

Equations

• List.scanlTR f a l = List.scanlTR.go f l a #[]

ink

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

• List.scanlTR.go f [] x x = Array.toListAppend x [x]
• List.scanlTR.go f (b :: l) x x = List.scanlTR.go f l (f x b) (Array.push x x)

ink

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

ink

@[csimp]

theorem List.scanl_eq_scanlTR : @List.scanl = @List.scanlTR

ink

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 => match x with | (b', l') => (f a b', b' :: l')) (b, []) l with | (b', l') => b' :: l'

ink

@[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 γ× 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])
⊕ Nat → Nat ⊕ Nat) [inl 0, inr 1, inl 2] = ([0, 2], [1])
→ Nat ⊕ Nat) [inl 0, inr 1, inl 2] = ([0, 2], [1])
⊕ Nat) [inl 0, inr 1, inl 2] = ([0, 2], [1])

Equations

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

ink

@[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 = (Array.toList x, Array.toList x)
• List.partitionMap.go f (x_3 :: xs) x x = match f x_3 with | Sum.inl a => List.partitionMap.go f xs (Array.push x a) x | Sum.inr b => List.partitionMap.go f xs x (Array.push x b)

ink

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

• List.foldlIdx f init [] x = init
• List.foldlIdx f init (b :: l) x = List.foldlIdx f (f x init b) l (x + 1)

ink

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

• List.foldrIdx f init [] x = init
• List.foldrIdx f init (b :: l) x = f x b (List.foldrIdx f init l (x + 1))

ink

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

• List.findIdxs p l = List.foldrIdx (fun i a is => if p a = true then i :: is else is) [] l

ink

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

• List.indexesValues p l = List.foldrIdx (fun i a l => if p a = true then (i, a) :: l else l) [] l

ink

@[inline]

def List.indexesOf {α : Type u_1} [inst : 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

• List.indexesOf a = List.findIdxs fun x => x == a

ink

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

• List.findIdx? p [] x = none
• List.findIdx? p (b :: l) x = if p b = true then some x else List.findIdx? p l (x + 1)

ink

@[inline]

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

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

Equations

• List.indexOf? a a = List.findIdx? (fun x => a == x) a

ink

@[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 α→ Option α to each element of the list, replacing a → b→ b at the first value a in the list such that f a = some b.

Equations

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

ink

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

• List.lookmap.go f [] x = Array.toList x
• List.lookmap.go f (x_2 :: xs) x = match f x_2 with | some b => Array.toListAppend x (b :: xs) | none => List.lookmap.go f xs (Array.push x x_2)

ink

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

• List.countp p l = List.countp.go p l 0

ink

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

• List.countp.go p [] x = x
• List.countp.go p (a :: l) x = bif p a then List.countp.go p l (x + 1) else List.countp.go p l x

ink

@[inline]

def List.count {α : Type u_1} [inst : BEq α] (a : α) : List α → Nat

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

Equations

• List.count a = List.countp fun x => x == a

ink

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

• (l₁ <+: l₂) = ∃ t, l₁ ++ t = l₂

ink

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

• (l₁ <:+ l₂) = ∃ t, t ++ l₁ = l₂

ink

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

• (l₁ <:+: l₂) = ∃ s t, s ++ l₁ ++ t = l₂

ink

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

• List.«term_<+:_» = Lean.ParserDescr.trailingNode `List.term_<+:_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <+: ") (Lean.ParserDescr.cat `term 51))

ink

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

• List.«term_<:+_» = Lean.ParserDescr.trailingNode `List.term_<:+_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <:+ ") (Lean.ParserDescr.cat `term 51))

ink

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

• List.«term_<:+:_» = Lean.ParserDescr.trailingNode `List.term_<:+:_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <:+: ") (Lean.ParserDescr.cat `term 51))

ink

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

• List.inits [] = [[]]
• List.inits (x_1 :: xs) = [] :: List.map (fun t => x_1 :: t) (List.inits xs)

ink

def List.initsTR {α : Type u_1} (l : List α) : List (List α)

Tail-recursive version of inits.

Equations

• List.initsTR l = Array.toListRev (List.foldr (fun a arrs => Array.push (Array.map (fun t => a :: t) arrs) []) #[[]] l)

ink

@[csimp]

theorem List.inits_eq_initsTR : @List.inits = @List.initsTR

ink

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

• List.tails [] = [[]]
• List.tails (x_1 :: xs) = (x_1 :: xs) :: List.tails xs

ink

def List.tailsTR {α : Type u_1} (l : List α) : List (List α)

Tail-recursive version of tails.

Equations

• List.tailsTR l = List.tailsTR.go l #[]

ink

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

• List.tailsTR.go [] acc = Array.toListAppend acc [[]]
• List.tailsTR.go (x_1 :: xs) acc = List.tailsTR.go xs (Array.push acc (x_1 :: xs))

ink

@[csimp]

theorem List.tails_eq_tailsTR : @List.tails = @List.tailsTR

ink

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

• List.sublists' l = let f := fun a arr => Array.foldl (fun r l => Array.push r (a :: l)) arr arr 0 (Array.size arr); Array.toList (List.foldr f #[[]] l)

ink

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

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

ink

inductive List.Forall₂ {α : Type u_1} {β : Type u_2} (R : α → β → Prop) : List α → List β → Prop

• Two nil lists are Forall₂-related

  nil: ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop}, List.Forall₂ R [] []

• Two cons lists are related by Forall₂ R if the heads are related by R and the tails are related by Forall₂ R

  cons: ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a : α} {b : β} {l₁ : List α} {l₂ : List β}, R a b → List.Forall₂ R l₁ l₂ → List.Forall₂ R (a :: l₁) (b :: l₂)

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.

ink

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

• List.transpose l = Array.toList (List.foldr List.transpose.go #[] l)

ink

def List.transpose.pop {α : Type u_1} (old : List α) : List α → Id (List α × List α)

pop : List α → StateM (List α) (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

• List.transpose.pop old x = match x with | [] => (old, []) | a :: l => (a :: old, l)

ink

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

go : List α → Array (List α) → Array (List α)→ Array (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

• List.transpose.go l acc = match Array.mapM List.transpose.pop acc l with | (acc, l) => List.foldl (fun arr a => Array.push arr [a]) acc l

ink

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

• List.sections [] = [[]]
• List.sections (l :: L) = List.bind (List.sections L) fun s => List.map (fun a => a :: s) l

ink

def List.sectionsTR {α : Type u_1} (L : List (List α)) : List (List α)

Optimized version of sections.

Equations

• List.sectionsTR L = bif List.any L List.isEmpty then [] else Array.toList (List.foldr List.sectionsTR.go #[[]] L)

ink

def List.sectionsTR.go {α : Type u_1} (l : List α) (acc : Array (List α)) : Array (List α)

go : List α → Array (List α) → Array (List α)→ Array (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

• List.sectionsTR.go l acc = Array.foldl (fun acc' l' => List.foldl (fun acc' a => Array.push acc' (a :: l')) acc' l) #[] acc 0 (Array.size acc)

ink

theorem List.sections_eq_nil_of_isEmpty {α : Type u_1} {L : List (List α)} : List.any L List.isEmpty = true → List.sections L = []

ink

@[csimp]

theorem List.sections_eq_sectionsTR : @List.sections = @List.sectionsTR

ink

def List.eraseP {α : Type u_1} (p : α → Bool) : List α → List α

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

Equations

• List.eraseP p [] = []
• List.eraseP p (x_1 :: xs) = bif p x_1 then xs else x_1 :: List.eraseP p xs

ink

@[inline]

def List.erasePTR {α : Type u_1} (p : α → Bool) (l : List α) : List α

Tail-recursive version of eraseP.

Equations

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

ink

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

• List.erasePTR.go p l [] x = l
• List.erasePTR.go p l (x_2 :: xs) x = bif p x_2 then Array.toListAppend x xs else List.erasePTR.go p l xs (Array.push x x_2)

ink

@[csimp]

theorem List.eraseP_eq_erasePTR : @List.eraseP = @List.erasePTR

ink

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

ink

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

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

ink

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

• List.extractP.go p l [] x = (none, l)
• List.extractP.go p l (x_2 :: xs) x = bif p x_2 then (some x_2, Array.toListAppend x xs) else List.extractP.go p l xs (Array.push x x_2)

ink

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

• List.revzip l = List.zip l (List.reverse l)

ink

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₁∈ l₁ and b ∈ l₂∈ l₂.

product [1, 2] [5, 6] = [(1, 5), (1, 6), (2, 5), (2, 6)]

Equations

• List.product l₁ l₂ = List.bind l₁ fun a => List.map (Prod.mk a) l₂

ink

def List.productTR {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) : List (α × β)

Optimized version of product.

Equations

• List.productTR l₁ l₂ = Array.toList (List.foldl (fun acc a => List.foldl (fun acc b => Array.push acc (a, b)) acc l₂) #[] l₁)

ink

@[csimp]

theorem List.product_eq_productTR : @List.product = @List.productTR

ink

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₁∈ l₁ and b ∈ l₂ a∈ l₂ a.

sigma [1, 2] (λ_, [(5 : Nat), 6]) = [(1, 5), (1, 6), (2, 5), (2, 6)]

Equations

• List.sigma l₁ l₂ = List.bind l₁ fun a => List.map (Sigma.mk a) (l₂ a)

ink

def List.sigmaTR {α : Type u_1} {σ : α → Type u_2} (l₁ : List α) (l₂ : (a : α) → List (σ a)) : List ((a : α) × σ a)

Optimized version of sigma.

Equations

• List.sigmaTR l₁ l₂ = Array.toList (List.foldl (fun acc a => List.foldl (fun acc b => Array.push acc { fst := a, snd := b }) acc (l₂ a)) #[] l₁)

ink

@[csimp]

theorem List.sigma_eq_sigmaTR : @List.sigma = @List.sigmaTR

ink

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

• List.ofFn f = Array.toList (Array.ofFn f)

ink

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

• List.ofFnNthVal f i = if h : i < n then some (f { val := i, isLt := h }) else none

ink

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

• List.Disjoint l₁ l₂ = ∀ ⦃a : α⦄, a ∈ l₁ → a ∈ l₂ → False

ink

inductive List.Pairwise {α : Type u_1} (R : α → α → Prop) : List α → Prop

• All elements of the empty list are vacuously pairwise related.

  nil: ∀ {α : Type u_1} {R : α → α → Prop}, List.Pairwise R []

• a :: l is Pairwise R if a R-relates to every element of l, and l is Pairwise R.

  cons: ∀ {α : Type u_1} {R : α → α → Prop} {a : α} {l : List α}, (∀ (a' : α), a' ∈ l → R a a') → List.Pairwise R l → List.Pairwise R (a :: l)

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
↔ R 1 2 ∧ R 1 3 ∧ R 2 3
∧ R 1 3 ∧ R 2 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.

ink

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

ink

instance List.instDecidablePairwise {α : Type u_1} {R : α → α → Prop} [inst : DecidableRel R] (l : List α) : Decidable (List.Pairwise R l)

Equations

• One or more equations did not get rendered due to their size.
• List.instDecidablePairwise [] = isTrue (_ : List.Pairwise R [])

ink

def List.pwFilter {α : Type u_1} (R : α → α → Prop) [inst : 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

• List.pwFilter R l = List.foldr (fun x IH => if (y : α) → y ∈ IH → R x y then x :: IH else IH) [] l

ink

inductive List.Chain {α : Type u_1} (R : α → α → Prop) : α → List α → Prop

• A chain of length 1 is trivially a chain.

  nil: ∀ {α : Type u_1} {R : α → α → Prop} {a : α}, List.Chain R a []

• If a relates to b and b::l is a chain, then a :: b :: l is also 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)

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
↔ R a b ∧ R b c ∧ R c d
∧ R b c ∧ R c d
∧ R c d

ink

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
↔ R a b ∧ R b c ∧ R c d
∧ R b c ∧ R c d
∧ R c d

Equations

• List.Chain' R x = match x with | [] => True | a :: l => List.Chain R a l

ink

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

• List.Nodup = List.Pairwise fun x x_1 => x ≠ x_1

ink

instance List.nodupDecidable {α : Type u_1} [inst : DecidableEq α] (l : List α) : Decidable (List.Nodup l)

Equations

• List.nodupDecidable = List.instDecidablePairwise

ink

@[inline]

def List.eraseDup {α : Type u_1} [inst : DecidableEq α] : 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

• List.eraseDup = List.pwFilter fun x x_1 => x ≠ x_1

ink

def List.range' : Nat → Nat → List Nat

range' s n is the list of numbers [s, s+1, ..., s+n-1]. It is intended mainly for proving properties of range and iota.

Equations

• List.range' x 0 = []
• List.range' x (Nat.succ n) = x :: List.range' (x + 1) n

ink

@[inline]

def List.range'TR (s : Nat) (n : Nat) : List Nat

Optimized version of range'.

Equations

• List.range'TR s n = List.range'TR.go n (s + n) []

ink

def List.range'TR.go : Nat → Nat → List Nat → List Nat

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

Equations

• List.range'TR.go 0 x x = x
• List.range'TR.go (Nat.succ n) x x = List.range'TR.go n (x - 1) ((x - 1) :: x)

ink

@[csimp]

theorem List.range'_eq_range'TR : List.range' = List.range'TR

ink

theorem List.range'_eq_range'TR.go (s : Nat) (n : Nat) (m : Nat) : List.range'TR.go n (s + n) (List.range' (s + n) m) = List.range' s (n + m)

ink

@[inline]

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

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

Equations

• List.reduceOption = List.filterMap id

ink

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.

Equations

• List.ilast' x [] = x
• List.ilast' x (b :: l) = List.ilast' b l

ink

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.

Equations

• List.last' [] = none
• List.last' [a] = some a
• List.last' (head :: l) = List.last' l

ink

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

• List.rotate l n = match List.splitAt (n % List.length l) l with | (l₁, l₂) => l₂ ++ l₁

ink

def List.rotate' {α : Type u_1} : List α → Nat → List α

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

Equations

• List.rotate' [] x = []
• List.rotate' x 0 = x
• List.rotate' (a :: l) (Nat.succ n) = List.rotate' (l ++ [a]) n

ink

def List.mapDiagM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → α → m β) (l : List α) : m (List β)

mapDiagM f l calls f on all elements in the upper triangular part of l × l× l. That is, for each e ∈ l∈ 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]
← f 1 1, ← f 1 2, ← f 1 3, ← f 2 2, ← f 2 3, ← f 3 3]
← f 1 2, ← f 1 3, ← f 2 2, ← f 2 3, ← f 3 3]
← f 1 3, ← f 2 2, ← f 2 3, ← f 3 3]
← f 2 2, ← f 2 3, ← f 3 3]
← f 2 3, ← f 3 3]
← f 3 3]

Equations

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

ink

def List.mapDiagM.go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → α → m β) : List α → Array β → m (List β)

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

Equations

• List.mapDiagM.go f [] x = pure (Array.toList x)
• List.mapDiagM.go f (x_2 :: xs) x = do let b ← f x_2 x_2 let acc ← List.foldlM (fun x x_1 => Array.push x <$> f x_2 x_1) (Array.push x b) xs List.mapDiagM.go f xs acc

ink

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

forDiagM f l calls f on all elements in the upper triangular part of l × l× l. That is, for each e ∈ l∈ 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

• List.forDiagM f [] = pure PUnit.unit
• List.forDiagM f (x_1 :: xs) = do f x_1 x_1 List.forM xs (f x_1) List.forDiagM f xs

ink

def List.getRest {α : Type u_1} [inst : 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

• List.getRest x [] = some x
• List.getRest [] x = none
• List.getRest (x_2 :: l) (y :: l₁) = if x_2 = y then List.getRest l l₁ else none

ink

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

• List.dropSlice x x [] = []
• List.dropSlice 0 x x = List.drop x x
• List.dropSlice (Nat.succ n) x (x_3 :: xs) = x_3 :: List.dropSlice n x xs

ink

@[inline]

def List.dropSliceTR {α : Type u_1} (n : Nat) (m : Nat) (l : List α) : List α

Optimized version of dropSlice.

Equations

• List.dropSliceTR n m l = match m with | 0 => l | Nat.succ m => List.dropSliceTR.go l m l n #[]

ink

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≥ length xs, in which case it is l.

Equations

• List.dropSliceTR.go l m [] x x = l
• List.dropSliceTR.go l m (head :: xs) 0 x = Array.toListAppend x (List.drop m xs)
• List.dropSliceTR.go l m (x_3 :: xs) (Nat.succ n) x = List.dropSliceTR.go l m xs n (Array.push x x_3)

ink

theorem List.dropSlice_zero₂ {α : Type u_1} (n : Nat) (l : List α) : List.dropSlice n 0 l = l

ink

@[csimp]

theorem List.dropSlice_eq_dropSliceTR : @List.dropSlice = @List.dropSliceTR

ink

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

ink

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∈ as and bᵢ ∈ bs∈ 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

• List.zipWithLeft' f [] x = ([], x)
• List.zipWithLeft' f (a :: as) [] = (List.map (fun a => f a none) (a :: as), [])
• List.zipWithLeft' f (a :: as) (b :: bs) = let r := List.zipWithLeft' f as bs; (f a (some b) :: r.fst, r.snd)

ink

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

• List.zipWithLeft'TR f as bs = List.zipWithLeft'TR.go f as bs #[]

ink

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

• List.zipWithLeft'TR.go f [] x x = (Array.toList x, x)
• List.zipWithLeft'TR.go f x [] x = (Array.toList (List.foldl (fun acc a => Array.push acc (f a none)) x x), [])
• List.zipWithLeft'TR.go f (a :: as) (b :: bs) x = List.zipWithLeft'TR.go f as bs (Array.push x (f a (some b)))

ink

@[csimp]

theorem List.zipWithLeft'_eq_zipWithLeft'TR : @List.zipWithLeft' = @List.zipWithLeft'TR

ink

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) => (Array.toList acc ++ l, r)

ink

@[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∈ as and bᵢ ∈ bs∈ 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

• List.zipWithRight' f as bs = List.zipWithLeft' (flip f) bs as

ink

@[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∈ as and bᵢ ∈ bs∈ 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

• List.zipLeft' = List.zipWithLeft' Prod.mk

ink

@[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∈ as and bᵢ ∈ bs∈ 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

• List.zipRight' = List.zipWithRight' Prod.mk

ink

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∈ as and bᵢ ‌∈ bs‌∈ 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

• List.zipWithLeft f [] x = []
• List.zipWithLeft f (a :: as) [] = List.map (fun a => f a none) (a :: as)
• List.zipWithLeft f (a :: as) (b :: bs) = f a (some b) :: List.zipWithLeft f as bs

ink

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

• List.zipWithLeftTR f as bs = List.zipWithLeftTR.go f as bs #[]

ink

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

• List.zipWithLeftTR.go f [] x x = Array.toList x
• List.zipWithLeftTR.go f x [] x = Array.toList (List.foldl (fun acc a => Array.push acc (f a none)) x x)
• List.zipWithLeftTR.go f (a :: as) (b :: bs) x = List.zipWithLeftTR.go f as bs (Array.push x (f a (some b)))

ink

@[csimp]

theorem List.zipWithLeft_eq_zipWithLeftTR : @List.zipWithLeft = @List.zipWithLeftTR

ink

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 = Array.toList acc ++ List.zipWithLeft f as bs

ink

@[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∈ as and bᵢ ‌∈ bs‌∈ 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

• List.zipWithRight f as bs = List.zipWithLeft (flip f) bs as

ink

@[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∈ as and bᵢ ∈ bs∈ 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

• List.zipLeft = List.zipWithLeft Prod.mk

ink

@[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∈ as and bᵢ ∈ bs∈ 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

• List.zipRight = List.zipWithRight Prod.mk

ink

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

• List.allSome l = List.mapM id l

ink

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

• List.fillNones [] x = []
• List.fillNones (some a :: as) x = a :: List.fillNones as x
• List.fillNones (none :: as) [] = List.reduceOption as
• List.fillNones (none :: as) (a :: as') = a :: List.fillNones as as'

ink

@[inline]

def List.fillNonesTR {α : Type u_1} (as : List (Option α)) (as' : List α) : List α

Tail-recursive version of fillNones.

Equations

• List.fillNonesTR as as' = List.fillNonesTR.go as as' #[]

ink

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

• List.fillNonesTR.go [] x x = Array.toList x
• List.fillNonesTR.go (some a :: as) x x = List.fillNonesTR.go as x (Array.push x a)
• List.fillNonesTR.go (none :: as) [] x = List.filterMapTR.go id as x
• List.fillNonesTR.go (none :: as) (a :: as') x = List.fillNonesTR.go as as' (Array.push x a)

ink

@[csimp]

theorem List.fillNones_eq_fillNonesTR : @List.fillNones = @List.fillNonesTR

ink

theorem List.fillNones_eq_fillNonesTR.go (α : Type u_1) (acc : Array α) (as : List (Option α)) (as' : List α) : List.fillNonesTR.go as as' acc = acc.data ++ List.fillNones as as'

ink

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

• List.takeList x [] = ([], x)
• List.takeList x (n :: ns) = match List.splitAt n x with | (xs₁, xs₂) => match List.takeList xs₂ ns with | (xss, rest) => (xs₁ :: xss, rest)

ink

@[inline]

def List.takeListTR {α : Type u_1} (xs : List α) (ns : List Nat) : List (List α) × List α

Tail-recursive version of takeList.

Equations

• List.takeListTR xs ns = List.takeListTR.go ns xs #[]

ink

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

• List.takeListTR.go [] x x = (Array.toList x, x)
• List.takeListTR.go (n :: ns) x x = match List.splitAt n x with | (xs₁, xs₂) => List.takeListTR.go ns xs₂ (Array.push x xs₁)

ink

@[csimp]

theorem List.takeList_eq_takeListTR : @List.takeList = @List.takeListTR

ink

theorem List.takeList_eq_takeListTR.go (α : Type u_1) (acc : Array (List α)) (ns : List Nat) (xs : List α) : List.takeListTR.go ns xs acc = match List.takeList xs ns with | (l, r) => (Array.toList acc ++ l, r)

ink

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

• List.toChunksAux n [] x = ([], [])
• List.toChunksAux n (head :: xs) 0 = match List.toChunksAux n xs n with | (l, L) => ([], (head :: l) :: L)
• List.toChunksAux n (x_2 :: xs) (Nat.succ i) = match List.toChunksAux n xs i with | (l, L) => (x_2 :: l, L)

ink

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

• List.toChunks x x = match x, x with | x, [] => [] | 0, xs => [xs] | n, x :: xs => List.toChunks.go n xs #[x] #[]

ink

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

• One or more equations did not get rendered due to their size.
• List.toChunks.go n [] x x = Array.toList (Array.push x (Array.toList x))

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.

ink

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

• List.zipWith₃ f (x_3 :: xs) (y :: ys) (z :: zs) = f x_3 y z :: List.zipWith₃ f xs ys zs
• List.zipWith₃ f x x x = []

ink

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

• List.zipWith₄ f (x_4 :: xs) (y :: ys) (z :: zs) (u :: us) = f x_4 y z u :: List.zipWith₄ f xs ys zs us
• List.zipWith₄ f x x x x = []

ink

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

• List.zipWith₅ f (x_5 :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) = f x_5 y z u v :: List.zipWith₅ f xs ys zs us vs
• List.zipWith₅ f x x x x x = []

ink

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

An auxiliary function for List.mapWithPrefixSuffix.

Equations

• List.mapWithPrefixSuffixAux f x [] = []
• List.mapWithPrefixSuffixAux f x (a :: l₂) = f x a l₂ :: List.mapWithPrefixSuffixAux f (List.concat x a) l₂

ink

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∈ l with l = pref ++ [a] ++ suff, a is mapped to f pref a suff. Example: if f : list Nat → Nat → list Nat → β→ Nat → list 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

• List.mapWithPrefixSuffix f l = List.mapWithPrefixSuffixAux f [] l

ink

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∈ 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 Nat → β→ β, List.mapWithComplement f [1, 2, 3] will produce the list [f 1 [2, 3], f 2 [1, 3], f 3 [1, 2]].

Equations

• List.mapWithComplement f = List.mapWithPrefixSuffix fun pref a suff => f a (pref ++ suff)