Documentation

Mathlib.Init.Data.List.Basic

Definitions for List not (yet) in Batteries

def List.headI {α : Type u_1} [Inhabited α] :
List αα

The head of a list, or the default element of the type is the list is nil.

Equations
  • x.headI = match x with | [] => default | a :: tail => a
Instances For
    @[simp]
    theorem List.headI_nil {α : Type u_1} [Inhabited α] :
    [].headI = default
    @[simp]
    theorem List.headI_cons {α : Type u_1} [Inhabited α] {h : α} {t : List α} :
    (h :: t).headI = h
    def List.getLastI {α : Type u_1} [Inhabited α] :
    List αα

    The last element of a list, with the default if list empty

    Equations
    • [].getLastI = default
    • [a].getLastI = a
    • [head, b].getLastI = b
    • (head :: head_1 :: l).getLastI = l.getLastI
    Instances For
      @[inline, deprecated List.pure]
      def List.ret {α : Type u} (a : α) :
      List α

      List with a single given element.

      Equations
      Instances For
        theorem List.le_eq_not_gt {α : Type u_1} [LT α] (l₁ : List α) (l₂ : List α) :
        (l₁ l₂) = ¬l₂ < l₁

        implies not > for lists.

        @[deprecated Array.data_toArray]
        theorem List.toArray_data {α : Type u_1} (as : List α) :
        (List.toArray as).data = as

        Alias of Array.data_toArray.