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)