## Tail recursive implementations for definitions from core #

Tail recursive version of `erase`

.

## Equations

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

## Instances For

Auxiliary for `setTR`

: `setTR.go l a xs n acc = acc.toList ++ set xs a`

,
unless `n ≥ 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)

## Instances For

Tail recursive version of `erase`

.

## Equations

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

## Instances For

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)

## Instances For

Tail recursive version of `eraseIdx`

.

## Equations

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

## Instances For

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)

## Instances For

Tail recursive version of `bind`

.

## Equations

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

## Instances For

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)

## Instances For

Tail recursive version of `filterMap`

.

## Equations

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

## Instances For

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)

## Instances For

Tail recursive version of `replace`

.

## Equations

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

## Instances For

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)

## Instances For

Tail recursive version of `take`

.

## Equations

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

## Instances For

Auxiliary for `take`

: `take.go l xs n acc = acc.toList ++ take n xs`

,
unless `n ≥ 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)

## Instances For

Tail recursive version of `takeWhile`

.

## Equations

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

## Instances For

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

## Instances For

Tail recursive version of `foldr`

.

## Equations

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

## Instances For

Tail recursive version of `zipWith`

.

## Equations

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

## Instances For

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

## Instances For

Tail recursive version of `dropLast`

.

## Equations

## Instances For

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 #[]

## Instances For

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)

## Instances For

## New definitions #

`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₂

## Instances For

## Equations

- One or more equations did not get rendered due to their size.
- List.decidableBAll p [] = isTrue (_ : ∀ (a : α), a ∈ [] → p a)

## Equations

- List.instDecidableRelListSubsetInstHasSubsetList x✝ x = List.decidableBAll (fun (a : α) => a ∈ x) x✝

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

## Instances For

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 #[]

## Instances For

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))

## Instances For

Monadic variant of `mapIdx`

.

## Equations

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

## Instances For

Auxiliary for `mapIdxM`

:
`mapIdxM.go as f acc = acc.toList ++ [← f acc.size 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)

## Instances For

`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

## Instances For

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

## Instances For

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)

## Instances For

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 : α) => x == a

## Instances For

Removes the `n`

th 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

## Instances For

Tail recursive version of `removeNth`

.

## Equations

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

## Instances For

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)

## Instances For

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

## Instances For

Tail-recursive version of `replaceF`

.

## Equations

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

## Instances For

Auxiliary for `replaceFTR`

: `replaceFTR.go f xs acc = acc.toList ++ replaceF f xs`

.

## Equations

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

## Instances For

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₁

## Instances For

## Equations

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

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₁

## Instances For

## Equations

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

`l₁ <+ l₂`

, or `Sublist l₁ l₂`

, says that `l₁`

is a (non-contiguous) subsequence of `l₂`

.

- slnil: ∀ {α : Type u_1}, List.Sublist [] []
the base case:

`[]`

is a sublist of`[]`

- 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 it is also a subsequence of`a :: l₂`

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

`l₁`

is a subsequence of`l₂`

, then`a :: l₁`

is a subsequence of`a :: l₂`

.

## Instances For

`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))

## Instances For

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

## Equations

- List.isSublist [] x = true
- List.isSublist x [] = false
- List.isSublist (hd₁ :: tl₁) (hd₂ :: tl₂) = if hd₁ = hd₂ then List.isSublist tl₁ tl₂ else List.isSublist (hd₁ :: tl₁) tl₂

## Instances For

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 #[]

## Instances For

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✝¹)

## Instances For

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 #[]

## Instances For

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), [])

## Instances For

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

## Instances For

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

- List.splitOnP.go P [] x = [List.reverse x]
- List.splitOnP.go P (a :: t) x = if P a = true then List.reverse x :: List.splitOnP.go P t [] else List.splitOnP.go P t (a :: x)

## Instances For

Tail recursive version of `removeNth`

.

## Equations

- List.splitOnPTR P l = List.splitOnPTR.go P l #[] #[]

## Instances For

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.splitOnPTR.go P [] x✝ x = Array.toListAppend x [Array.toList x✝]
- List.splitOnPTR.go P (a :: t) x✝ x = bif P a then List.splitOnPTR.go P t #[] (Array.push x (Array.toList x✝)) else List.splitOnPTR.go P t (Array.push x✝ a) x

## Instances For

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

## Instances For

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

## Instances For

Apply `f`

to the head of the list, if it exists.

## Equations

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

## Instances For

Apply `f`

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

## Equations

## Instances For

Tail-recursive version of `modifyNth`

.

## Equations

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

## Instances For

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)

## Instances For

Apply `f`

to the last element of `l`

, if it exists.

## Equations

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

## Instances For

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)

## Instances For

`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

## Instances For

Tail-recursive version of `insertNth`

.

## Equations

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

## Instances For

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)

## Instances For

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

## Instances For

Tail-recursive version of `takeD`

.

## Equations

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

## Instances For

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)

## Instances For

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

## Instances For

Optimized version of `leftpad`

.

## Equations

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

## Instances For

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

## Instances For

Tail-recursive version of `scanl`

.

## Equations

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

## Instances For

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✝)

## Instances For

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'

## Instances For

Given a function `f : α → β ⊕ γ`

, `partitionMap f l`

maps the list by `f`

whilst partitioning the result it into a pair of lists, `List β × List γ`

,
partitioning the `.inl _`

into the left list, and the `.inr _`

into the right List.

```
partitionMap (id : Nat ⊕ Nat → Nat ⊕ Nat) [inl 0, inr 1, inl 2] = ([0, 2], [1])
```

## Equations

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

## Instances For

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)

## Instances For

Monadic generalization of `List.partition`

.

## Equations

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

## Instances For

Auxiliary for `partitionM`

:
`partitionM.go p l acc₁ acc₂`

returns `(acc₁.toList ++ left, acc₂.toList ++ right)`

if `partitionM p l`

returns `(left, right)`

.

## Equations

- List.partitionM.go p [] x✝ x = pure (Array.toList x✝, Array.toList x)
- List.partitionM.go p (x_3 :: xs) x✝ x = do let __do_lift ← p x_3 if __do_lift = true then List.partitionM.go p xs (Array.push x✝ x_3) x else List.partitionM.go p xs x✝ (Array.push x x_3)

## Instances For

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)

## Instances For

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))

## Instances For

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 : Nat) (a : α) (l : List (Nat × α)) => if p a = true then (i, a) :: l else l) [] l

## Instances For

`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

## Instances For

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)

## Instances For

Return the index of the first occurrence of `a`

in the list.

## Equations

- List.indexOf? a✝ a = List.findIdx? (fun (x : α) => x == a✝) a

## Instances For

`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

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

## Instances For

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)

## Instances For

`countP p l`

is the number of elements of `l`

that satisfy `p`

.

## Equations

- List.countP p l = List.countP.go p l 0

## Instances For

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

## Instances For

`count a l`

is the number of occurrences of `a`

in `l`

.

## Equations

- List.count a = List.countP fun (x : α) => x == a

## Instances For

`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))

## Instances For

`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))

## Instances For

`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))

## Instances For

`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 : List α) => x_1 :: t) (List.inits xs)

## Instances For

Tail-recursive version of `inits`

.

## Equations

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

## Instances For

`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

## Instances For

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))

## Instances For

`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

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

## Instances For

`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

- List.sublists l = List.foldr (fun (a : α) (acc : List (List α)) => List.bind acc fun (x : List α) => [x, a :: x]) [[]] l

## Instances For

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.

## Instances For

`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.

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

`Forall₂`

-related - 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₂)

## Instances For

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)

## Instances For

`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

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

## Instances For

`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

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

## Instances For

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 α) => List.map (fun (a : α) => a :: s) l

## Instances For

Optimized version of `sections`

.

## Equations

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

## Instances For

`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

## Instances For

Tail-recursive version of `eraseP`

.

## Equations

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

## Instances For

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)

## Instances For

`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 #[]

## Instances For

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)

## Instances For

`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)

## Instances For

`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

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

## Instances For

`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

## Instances For

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

- List.takeWhile₂ R (a :: as) (b :: bs) = if R a b = true then match List.takeWhile₂ R as bs with | (as', bs') => (a :: as', b :: bs') else ([], [])
- List.takeWhile₂ R x✝ x = ([], [])

## Instances For

Tail-recursive version of `takeWhile₂`

.

## Equations

- List.takeWhile₂TR R as bs = List.takeWhile₂TR.go R as bs [] []

## Instances For

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

- List.takeWhile₂TR.go R (a :: as) (b :: bs) x✝ x = bif R a b then List.takeWhile₂TR.go R as bs (a :: x✝) (b :: x) else (List.reverse x✝, List.reverse x)
- List.takeWhile₂TR.go R x✝² x✝¹ x✝ x = (List.reverse x✝, List.reverse x)

## Instances For

`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.

- nil: ∀ {α : Type u_1} {R : α → α → Prop}, List.Pairwise R []
All elements of the empty list are vacuously pairwise related.

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

## Instances For

## Equations

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

`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 : List α) => if ∀ (y : α), y ∈ IH → R x y then x :: IH else IH) [] l

## Instances For

`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

`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

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

## Instances For

`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

## Instances For

## Equations

- List.nodupDecidable = List.instDecidablePairwise

`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

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

## Instances For

Optimized version of `range'`

.

## Equations

- List.range'TR s n step = List.range'TR.go step n (s + step * n) []

## Instances For

Auxiliary for `range'TR`

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

.

## Equations

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

## Instances For

Drop `none`

s from a list, and replace each remaining `some a`

with `a`

.

## Equations

- List.reduceOption = List.filterMap id

## Instances For

`ilast' x xs`

returns the last element of `xs`

if `xs`

is non-empty; it returns `x`

otherwise.
Use `List.getLastD`

instead.

## Equations

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

## Instances For

`last' xs`

returns the last element of `xs`

if `xs`

is non-empty; it returns `none`

otherwise.
Use `List.getLast?`

instead

## Equations

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

## Instances For

`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₁

## Instances For

`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

## Instances For

`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

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

## Instances For

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 : Array β) (x_1 : α) => Array.push x <$> f x_2 x_1) (Array.push x b) xs List.mapDiagM.go f xs acc

## Instances For

`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

- 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

## Instances For

`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

## Instances For

`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

## Instances For

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 #[]

## Instances For

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

- 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)

## Instances For

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

- 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)

## Instances For

Tail-recursive version of `zipWithLeft'`

.

## Equations

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

## Instances For

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 : Array γ) (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)))

## Instances For

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

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

## Instances For

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

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

## Instances For

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

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

## Instances For

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

- 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

## Instances For

Tail-recursive version of `zipWithLeft`

.

## Equations

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

## Instances For

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 : Array γ) (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)))

## Instances For

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

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

## Instances For

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

- List.zipLeft = List.zipWithLeft Prod.mk

## Instances For

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

- List.zipRight = List.zipWithRight Prod.mk

## Instances For

`fillNones xs ys`

replaces the `none`

s in `xs`

with elements of `ys`

. If there
are not enough `ys`

to replace all the `none`

s, the remaining `none`

s 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'

## Instances For

Tail-recursive version of `fillNones`

.

## Equations

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

## Instances For

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)

## Instances For

`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)

## Instances For

Tail-recursive version of `takeList`

.

## Equations

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

## Instances For

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₁)

## Instances For

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)

## Instances For

`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] #[]

## Instances For

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✝))

## Instances For

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`

.

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 = []

## Instances For

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 = []

## Instances For

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 = []

## Instances For

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₂

## Instances For

`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

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

## Instances For

`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

- List.mapWithComplement f = List.mapWithPrefixSuffix fun (pref : List α) (a : α) (suff : List α) => f a (pref ++ suff)

## Instances For

Map each element of a `List`

to an action, evaluate these actions in order,
and collect the results.

## Equations

- List.traverse f [] = pure []
- List.traverse f (x_1 :: xs) = Seq.seq (List.cons <$> f x_1) fun (x : Unit) => List.traverse f xs

## Instances For

`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}, List.Perm [] []
`[] ~ []`

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

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

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

is transitive.

## Instances For

`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

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

## Instances For

`O(|l₁| * |l₂|)`

. Computes whether `l₁`

is a permutation of `l₂`

. See `isPerm_iff`

for a
characterization in terms of `List.Perm`

.

## Equations

- List.isPerm [] x = List.isEmpty x
- List.isPerm (a :: t) x = (List.contains x a && List.isPerm t (List.erase x a))

## Instances For

`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

- List.Subperm l₁ l₂ = ∃ (l : List α), List.Perm l l₁ ∧ List.Sublist l l₂

## Instances For

`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

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

## Instances For

`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

- List.isSubperm l₁ l₂ = decide (∀ (x : α), x ∈ l₁ → List.count x l₁ ≤ List.count x l₂)