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

## Instances For

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`

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

.

## Instances For

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

def
List.mapMonoM
{m : Type u_1 → Type u_2}
{α : Type u_1}
[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)