The following functions can't be defined at `Init.Data.List.Basic`

, because they depend on `Init.Util`

,
and `Init.Util`

depends on `Init.Data.List.Basic`

.

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

- List.getLast [] h = absurd ⋯ h
- List.getLast [a] x_2 = a
- List.getLast (head :: b :: as) x_2 = List.getLast (b :: as) ⋯

## Instances For

## Equations

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

## Instances For

## Equations

- List.getLast? x = match x with | [] => none | a :: as => some (List.getLast (a :: as) ⋯)

## Instances For

## Equations

- List.getLastD x✝ x = match x✝, x with | [], a₀ => a₀ | a :: as, x => List.getLast (a :: as) ⋯

## Instances For

## Equations

- List.rotateLeft xs n = let len := List.length xs; if len ≤ 1 then xs else let n := n % len; let b := List.take n xs; let e := List.drop n xs; e ++ b

## Instances For

This tactic, added to the `decreasing_trivial`

toolbox, proves that
`sizeOf a < sizeOf as`

when `a ∈ as`

, which is useful for well founded recursions
over a nested inductive like `inductive T | mk : List T → T`

.

## Equations

- List.tacticSizeOf_list_dec = Lean.ParserDescr.node `List.tacticSizeOf_list_dec 1024 (Lean.ParserDescr.nonReservedSymbol "sizeOf_list_dec" false)

## Instances For

Monomorphic `List.mapM`

. The internal implementation uses pointer equality, and does not allocate a new list
if the result of each `f a`

is a pointer equal value `a`

.

## Equations

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

## Instances For

## Equations

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

## Instances For

Monadic generalization of `List.partition`

.

This uses `Array.toList`

and which isn't imported by `Init.Data.List.Basic`

.

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

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)