Documentation

Mathlib.Init.Data.List.Basic

Definitions for List not (yet) in Std

@[deprecated List.get]
def List.nthLe {α : Type u_1} (l : List α) (n : ) (h : n < List.length l) :
α

nth element of a list l given n < l.length.

Equations
Instances For
    @[deprecated]
    theorem List.nthLe_eq {α : Type u_1} (l : List α) (n : ) (h : n < List.length l) :
    List.nthLe l n h = List.get l { val := n, isLt := h }
    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
    Instances For
      @[simp]
      theorem List.headI_nil {α : Type u_1} [Inhabited α] :
      List.headI [] = default
      @[simp]
      theorem List.headI_cons {α : Type u_1} [Inhabited α] {h : α} {t : List α} :
      List.headI (h :: t) = h
      @[deprecated List.findIdx]
      def List.findIndex {α : Type u_1} (p : αProp) [DecidablePred p] :
      List α

      Find index of element with given property.

      Equations
      Instances For
        def List.getLastI {α : Type u_1} [Inhabited α] :
        List αα

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

        Equations
        Instances For
          @[inline]
          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.