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!" 31 12 "empty list" | a :: tail => a

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

- List.getLast [] h = absurd (_ : [] = []) h
- List.getLast [a] x_2 = a
- List.getLast (head :: b :: as) x_2 = List.getLast (b :: as) (_ : b :: as = [] → List.noConfusionType False (b :: as) [])

## Equations

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

## Equations

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

## Equations

- List.getLastD x x = match x, x with | [], a₀ => a₀ | a :: as, x => List.getLast (a :: as) (_ : a :: as = [] → List.noConfusionType False (a :: as) [])

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

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

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

theorem
List.get_last
{α : Type u_1}
{a : α}
{as : List α}
{i : Fin (List.length (as ++ [a]))}
(h : ¬i.val < List.length as)
:

This tactic, added to the `decreasing_trivial`

toolbox, proves that
`sizeOf a < sizeOf as`

when `a ∈ as∈ as`

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

.

## Equations

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

@[implemented_by _private.Init.Data.List.BasicAux.0.List.mapMonoMImp]

def
List.mapMonoM
{m : Type u_1 → Type u_2}
{α : Type u_1}
[inst : Monad m]
(as : List α)
(f : α → m α)
:

m (List α)

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)

## Equations

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