Documentation

Init.Data.List.Basic

The syntax [a, b, c] is shorthand for a :: b :: c :: [], or List.cons a (List.cons b (List.cons c List.nil)). It allows conveniently constructing list literals.

For lists of length at least 64, an alternative desugaring strategy is used which uses let bindings as intermediates as in let left := [d, e, f]; a :: b :: c :: left to avoid creating very deep expressions. Note that this changes the order of evaluation, although it should not be observable unless you use side effecting operations like dbg_trace.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Auxiliary syntax for implementing [$elem,*] list literal syntax. The syntax %[a,b,c|tail] constructs a value equivalent to a::b::c::tail. It uses binary partitioning to construct a tree of intermediate let bindings as in let left := [d, e, f]; a :: b :: c :: left to avoid creating very deep expressions.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      instance List.instGetElemListNatLtInstLTNatLength {α : Type u} :
      GetElem (List α) Nat α fun (as : List α) (i : Nat) => i < List.length as
      Equations
      • List.instGetElemListNatLtInstLTNatLength = { getElem := fun (as : List α) (i : Nat) (h : i < List.length as) => List.get as { val := i, isLt := h } }
      @[simp]
      theorem List.cons_getElem_zero {α : Type u} (a : α) (as : List α) (h : 0 < List.length (a :: as)) :
      (a :: as)[0] = a
      @[simp]
      theorem List.cons_getElem_succ {α : Type u} (a : α) (as : List α) (i : Nat) (h : i + 1 < List.length (a :: as)) :
      (a :: as)[i + 1] = as[i]
      theorem List.length_add_eq_lengthTRAux {α : Type u} (as : List α) (n : Nat) :
      @[simp]
      theorem List.length_nil {α : Type u} :
      def List.reverseAux {α : Type u} :
      List αList αList α

      Auxiliary for List.reverse. List.reverseAux l r = l.reverse ++ r, but it is defined directly.

      Equations
      Instances For
        def List.reverse {α : Type u} (as : List α) :
        List α

        O(|as|). Reverse of a list:

        • [1, 2, 3, 4].reverse = [4, 3, 2, 1]

        Note that because of the "functional but in place" optimization implemented by Lean's compiler, this function works without any allocations provided that the input list is unshared: it simply walks the linked list and reverses all the node pointers.

        Equations
        Instances For
          theorem List.reverseAux_reverseAux {α : Type u} (as : List α) (bs : List α) (cs : List α) :
          @[simp]
          theorem List.reverse_reverse {α : Type u} (as : List α) :
          def List.append {α : Type u} (xs : List α) (ys : List α) :
          List α

          O(|xs|): append two lists. [1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5]. It takes time proportional to the first list.

          Equations
          Instances For
            def List.appendTR {α : Type u} (as : List α) (bs : List α) :
            List α

            Tail-recursive version of List.append.

            Equations
            Instances For
              instance List.instAppendList {α : Type u} :
              Equations
              • List.instAppendList = { append := List.append }
              @[simp]
              theorem List.nil_append {α : Type u} (as : List α) :
              [] ++ as = as
              @[simp]
              theorem List.append_nil {α : Type u} (as : List α) :
              as ++ [] = as
              @[simp]
              theorem List.cons_append {α : Type u} (a : α) (as : List α) (bs : List α) :
              a :: as ++ bs = a :: (as ++ bs)
              @[simp]
              theorem List.append_eq {α : Type u} (as : List α) (bs : List α) :
              List.append as bs = as ++ bs
              @[simp]
              theorem List.append_assoc {α : Type u} (as : List α) (bs : List α) (cs : List α) :
              as ++ bs ++ cs = as ++ (bs ++ cs)
              theorem List.append_cons {α : Type u} (as : List α) (b : α) (bs : List α) :
              as ++ b :: bs = as ++ [b] ++ bs
              Equations
              • List.instEmptyCollectionList = { emptyCollection := [] }
              def List.erase {α : Type u_1} [BEq α] :
              List ααList α

              O(|l|). erase l a removes the first occurrence of a from l.

              • erase [1, 5, 3, 2, 5] 5 = [1, 3, 2, 5]
              • erase [1, 5, 3, 2, 5] 6 = [1, 5, 3, 2, 5]
              Equations
              Instances For
                def List.eraseIdx {α : Type u} :
                List αNatList α

                O(i). eraseIdx l i removes the i'th element of the list l.

                • erase [a, b, c, d, e] 0 = [b, c, d, e]
                • erase [a, b, c, d, e] 1 = [a, c, d, e]
                • erase [a, b, c, d, e] 5 = [a, b, c, d, e]
                Equations
                Instances For
                  def List.isEmpty {α : Type u} :
                  List αBool

                  O(1). isEmpty l is true if the list is empty.

                  Equations
                  Instances For
                    @[specialize #[]]
                    def List.map {α : Type u} {β : Type v} (f : αβ) :
                    List αList β

                    O(|l|). map f l applies f to each element of the list.

                    • map f [a, b, c] = [f a, f b, f c]
                    Equations
                    Instances For
                      @[inline]
                      def List.mapTR {α : Type u} {β : Type v} (f : αβ) (as : List α) :
                      List β

                      Tail-recursive version of List.map.

                      Equations
                      Instances For
                        @[specialize #[]]
                        def List.mapTR.loop {α : Type u} {β : Type v} (f : αβ) :
                        List αList βList β
                        Equations
                        Instances For
                          theorem List.reverseAux_eq_append {α : Type u} (as : List α) (bs : List α) :
                          @[simp]
                          theorem List.reverse_nil {α : Type u} :
                          @[simp]
                          theorem List.reverse_cons {α : Type u} (a : α) (as : List α) :
                          @[simp]
                          theorem List.reverse_append {α : Type u} (as : List α) (bs : List α) :
                          theorem List.mapTR_loop_eq {α : Type u} {β : Type v} (f : αβ) (as : List α) (bs : List β) :
                          def List.join {α : Type u} :
                          List (List α)List α

                          O(|join L|). join L concatenates all the lists in L into one list.

                          • join [[a], [], [b, c], [d, e, f]] = [a, b, c, d, e, f]
                          Equations
                          Instances For
                            @[specialize #[]]
                            def List.filterMap {α : Type u} {β : Type v} (f : αOption β) :
                            List αList β

                            O(|l|). filterMap f l takes a function f : α → Option β and applies it to each element of l; the resulting non-none values are collected to form the output list.

                            filterMap
                              (fun x => if x > 2 then some (2 * x) else none)
                              [1, 2, 5, 2, 7, 7]
                            = [10, 14, 14]
                            
                            Equations
                            Instances For
                              def List.filter {α : Type u} (p : αBool) :
                              List αList α

                              O(|l|). filter f l returns the list of elements in l for which f returns true.

                              filter (· > 2) [1, 2, 5, 2, 7, 7] = [5, 7, 7]
                              
                              Equations
                              Instances For
                                @[inline]
                                def List.filterTR {α : Type u} (p : αBool) (as : List α) :
                                List α

                                Tail-recursive version of List.filter.

                                Equations
                                Instances For
                                  @[specialize #[]]
                                  def List.filterTR.loop {α : Type u} (p : αBool) :
                                  List αList αList α
                                  Equations
                                  Instances For
                                    theorem List.filterTR_loop_eq {α : Type u} (p : αBool) (as : List α) (bs : List α) :
                                    @[inline]
                                    def List.partition {α : Type u} (p : αBool) (as : List α) :
                                    List α × List α

                                    O(|l|). partition p l calls p on each element of l, partitioning the list into two lists (l_true, l_false) where l_true has the elements where p was true and l_false has the elements where p is false. partition p l = (filter p l, filter (not ∘ p) l), but it is slightly more efficient since it only has to do one pass over the list.

                                    partition (· > 2) [1, 2, 5, 2, 7, 7] = ([5, 7, 7], [1, 2, 2])
                                    
                                    Equations
                                    Instances For
                                      @[specialize #[]]
                                      def List.partition.loop {α : Type u} (p : αBool) :
                                      List αList α × List αList α × List α
                                      Equations
                                      Instances For
                                        def List.dropWhile {α : Type u} (p : αBool) :
                                        List αList α

                                        O(|l|). dropWhile p l removes elements from the list until it finds the first element for which p returns false; this element and everything after it is returned.

                                        dropWhile (· < 4) [1, 3, 2, 4, 2, 7, 4] = [4, 2, 7, 4]
                                        
                                        Equations
                                        Instances For
                                          def List.find? {α : Type u} (p : αBool) :
                                          List αOption α

                                          O(|l|). find? p l returns the first element for which p returns true, or none if no such element is found.

                                          • find? (· < 5) [7, 6, 5, 8, 1, 2, 6] = some 1
                                          • find? (· < 1) [7, 6, 5, 8, 1, 2, 6] = none
                                          Equations
                                          Instances For
                                            def List.findSome? {α : Type u} {β : Type v} (f : αOption β) :
                                            List αOption β

                                            O(|l|). findSome? f l applies f to each element of l, and returns the first non-none result.

                                            • findSome? (fun x => if x < 5 then some (10 * x) else none) [7, 6, 5, 8, 1, 2, 6] = some 10
                                            Equations
                                            Instances For
                                              def List.replace {α : Type u} [BEq α] :
                                              List αααList α

                                              O(|l|). replace l a b replaces the first element in the list equal to a with b.

                                              • replace [1, 4, 2, 3, 3, 7] 3 6 = [1, 4, 2, 6, 3, 7]
                                              • replace [1, 4, 2, 3, 3, 7] 5 6 = [1, 4, 2, 3, 3, 7]
                                              Equations
                                              Instances For
                                                def List.elem {α : Type u} [BEq α] (a : α) :
                                                List αBool

                                                O(|l|). elem a l or l.contains a is true if there is an element in l equal to a.

                                                • elem 3 [1, 4, 2, 3, 3, 7] = true
                                                • elem 5 [1, 4, 2, 3, 3, 7] = false
                                                Equations
                                                Instances For
                                                  def List.notElem {α : Type u} [BEq α] (a : α) (as : List α) :

                                                  notElem a l is !(elem a l).

                                                  Equations
                                                  Instances For
                                                    @[inline, reducible]
                                                    abbrev List.contains {α : Type u} [BEq α] (as : List α) (a : α) :

                                                    O(|l|). elem a l or l.contains a is true if there is an element in l equal to a.

                                                    • elem 3 [1, 4, 2, 3, 3, 7] = true
                                                    • elem 5 [1, 4, 2, 3, 3, 7] = false
                                                    Equations
                                                    Instances For
                                                      inductive List.Mem {α : Type u} (a : α) :
                                                      List αProp

                                                      a ∈ l is a predicate which asserts that a is in the list l. Unlike elem, this uses = instead of == and is suited for mathematical reasoning.

                                                      • a ∈ [x, y, z] ↔ a = x ∨ a = y ∨ a = z
                                                      • head: ∀ {α : Type u} {a : α} (as : List α), List.Mem a (a :: as)

                                                        The head of a list is a member: a ∈ a :: as.

                                                      • tail: ∀ {α : Type u} {a : α} (b : α) {as : List α}, List.Mem a asList.Mem a (b :: as)

                                                        A member of the tail of a list is a member of the list: a ∈ l → a ∈ b :: l.

                                                      Instances For
                                                        instance List.instMembershipList {α : Type u} :
                                                        Equations
                                                        • List.instMembershipList = { mem := List.Mem }
                                                        theorem List.mem_of_elem_eq_true {α : Type u} [BEq α] [LawfulBEq α] {a : α} {as : List α} :
                                                        List.elem a as = truea as
                                                        theorem List.elem_eq_true_of_mem {α : Type u} [BEq α] [LawfulBEq α] {a : α} {as : List α} (h : a as) :
                                                        theorem List.mem_append_of_mem_left {α : Type u} {a : α} {as : List α} (bs : List α) :
                                                        a asa as ++ bs
                                                        theorem List.mem_append_of_mem_right {α : Type u} {b : α} {bs : List α} (as : List α) :
                                                        b bsb as ++ bs
                                                        def List.eraseDups {α : Type u_1} [BEq α] (as : List α) :
                                                        List α

                                                        O(|l|^2). Erase duplicated elements in the list. Keeps the first occurrence of duplicated elements.

                                                        • eraseDups [1, 3, 2, 2, 3, 5] = [1, 3, 2, 5]
                                                        Equations
                                                        Instances For
                                                          def List.eraseDups.loop {α : Type u_1} [BEq α] :
                                                          List αList αList α
                                                          Equations
                                                          Instances For
                                                            def List.eraseReps {α : Type u_1} [BEq α] :
                                                            List αList α

                                                            O(|l|). Erase repeated adjacent elements. Keeps the first occurrence of each run.

                                                            • eraseReps [1, 3, 2, 2, 2, 3, 5] = [1, 3, 2, 3, 5]
                                                            Equations
                                                            Instances For
                                                              def List.eraseReps.loop {α : Type u_1} [BEq α] :
                                                              αList αList αList α
                                                              Equations
                                                              Instances For
                                                                @[inline]
                                                                def List.span {α : Type u} (p : αBool) (as : List α) :
                                                                List α × List α

                                                                O(|l|). span p l splits the list l into two parts, where the first part contains the longest initial segment for which p returns true and the second part is everything else.

                                                                • span (· > 5) [6, 8, 9, 5, 2, 9] = ([6, 8, 9], [5, 2, 9])
                                                                • span (· > 10) [6, 8, 9, 5, 2, 9] = ([6, 8, 9, 5, 2, 9], [])
                                                                Equations
                                                                Instances For
                                                                  @[specialize #[]]
                                                                  def List.span.loop {α : Type u} (p : αBool) :
                                                                  List αList αList α × List α
                                                                  Equations
                                                                  Instances For
                                                                    @[specialize #[]]
                                                                    def List.groupBy {α : Type u} (R : ααBool) :
                                                                    List αList (List α)

                                                                    O(|l|). groupBy R l splits l into chains of elements such that adjacent elements are related by R.

                                                                    • groupBy (·==·) [1, 1, 2, 2, 2, 3, 2] = [[1, 1], [2, 2, 2], [3], [2]]
                                                                    • groupBy (·<·) [1, 2, 5, 4, 5, 1, 4] = [[1, 2, 5], [4, 5], [1, 4]]
                                                                    Equations
                                                                    Instances For
                                                                      @[specialize #[]]
                                                                      def List.groupBy.loop {α : Type u} (R : ααBool) :
                                                                      List ααList αList (List α)List (List α)
                                                                      Equations
                                                                      Instances For
                                                                        def List.lookup {α : Type u} {β : Type v} [BEq α] :
                                                                        αList (α × β)Option β

                                                                        O(|l|). lookup a l treats l : List (α × β) like an association list, and returns the first β value corresponding to an α value in the list equal to a.

                                                                        • lookup 3 [(1, 2), (3, 4), (3, 5)] = some 4
                                                                        • lookup 2 [(1, 2), (3, 4), (3, 5)] = none
                                                                        Equations
                                                                        Instances For
                                                                          def List.removeAll {α : Type u} [BEq α] (xs : List α) (ys : List α) :
                                                                          List α

                                                                          O(|xs|). Computes the "set difference" of lists, by filtering out all elements of xs which are also in ys.

                                                                          • removeAll [1, 1, 5, 1, 2, 4, 5] [1, 2, 2] = [5, 4, 5]
                                                                          Equations
                                                                          Instances For
                                                                            def List.drop {α : Type u} :
                                                                            NatList αList α

                                                                            O(min n |xs|). Removes the first n elements of xs.

                                                                            • drop 0 [a, b, c, d, e] = [a, b, c, d, e]
                                                                            • drop 3 [a, b, c, d, e] = [d, e]
                                                                            • drop 6 [a, b, c, d, e] = []
                                                                            Equations
                                                                            Instances For
                                                                              @[simp]
                                                                              theorem List.drop_nil {α : Type u} {i : Nat} :
                                                                              List.drop i [] = []
                                                                              theorem List.get_drop_eq_drop {α : Type u} (as : List α) (i : Nat) (h : i < List.length as) :
                                                                              as[i] :: List.drop (i + 1) as = List.drop i as
                                                                              def List.take {α : Type u} :
                                                                              NatList αList α

                                                                              O(min n |xs|). Returns the first n elements of xs, or the whole list if n is too large.

                                                                              • take 0 [a, b, c, d, e] = []
                                                                              • take 3 [a, b, c, d, e] = [a, b, c]
                                                                              • take 6 [a, b, c, d, e] = [a, b, c, d, e]
                                                                              Equations
                                                                              Instances For
                                                                                def List.takeWhile {α : Type u} (p : αBool) (xs : List α) :
                                                                                List α

                                                                                O(|xs|). Returns the longest initial segment of xs for which p returns true.

                                                                                Equations
                                                                                Instances For
                                                                                  @[specialize #[]]
                                                                                  def List.foldr {α : Type u} {β : Type v} (f : αββ) (init : β) :
                                                                                  List αβ

                                                                                  O(|l|). Applies function f to all of the elements of the list, from right to left.

                                                                                  • foldr f init [a, b, c] = f a <| f b <| f c <| init
                                                                                  Equations
                                                                                  Instances For
                                                                                    def List.any {α : Type u} :
                                                                                    List α(αBool)Bool

                                                                                    O(|l|). Returns true if p is true for any element of l.

                                                                                    • any p [a, b, c] = p a || p b || p c

                                                                                    Short-circuits upon encountering the first true.

                                                                                    Equations
                                                                                    Instances For
                                                                                      def List.all {α : Type u} :
                                                                                      List α(αBool)Bool

                                                                                      O(|l|). Returns true if p is true for every element of l.

                                                                                      • all p [a, b, c] = p a && p b && p c

                                                                                      Short-circuits upon encountering the first false.

                                                                                      Equations
                                                                                      Instances For
                                                                                        def List.or (bs : List Bool) :

                                                                                        O(|l|). Returns true if true is an element of the list of booleans l.

                                                                                        • or [a, b, c] = a || b || c
                                                                                        Equations
                                                                                        Instances For
                                                                                          def List.and (bs : List Bool) :

                                                                                          O(|l|). Returns true if every element of l is the value true.

                                                                                          • and [a, b, c] = a && b && c
                                                                                          Equations
                                                                                          Instances For
                                                                                            @[specialize #[]]
                                                                                            def List.zipWith {α : Type u} {β : Type v} {γ : Type w} (f : αβγ) (xs : List α) (ys : List β) :
                                                                                            List γ

                                                                                            O(min |xs| |ys|). Applies f to the two lists in parallel, stopping at the shorter list.

                                                                                            • zipWith f [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [f x₁ y₁, f x₂ y₂, f x₃ y₃]
                                                                                            Equations
                                                                                            Instances For
                                                                                              def List.zip {α : Type u} {β : Type v} :
                                                                                              List αList βList (α × β)

                                                                                              O(min |xs| |ys|). Combines the two lists into a list of pairs, with one element from each list. The longer list is truncated to match the shorter list.

                                                                                              • zip [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]
                                                                                              Equations
                                                                                              Instances For
                                                                                                def List.zipWithAll {α : Type u} {β : Type v} {γ : Type w} (f : Option αOption βγ) :
                                                                                                List αList βList γ

                                                                                                O(max |xs| |ys|). Version of List.zipWith that continues to the end of both lists, passing none to one argument once the shorter list has run out.

                                                                                                Equations
                                                                                                Instances For
                                                                                                  @[simp]
                                                                                                  theorem List.zipWithAll_nil_right :
                                                                                                  ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option αOption α_1α_2} {as : List α}, List.zipWithAll f as [] = List.map (fun (a : α) => f (some a) none) as
                                                                                                  @[simp]
                                                                                                  theorem List.zipWithAll_nil_left :
                                                                                                  ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option αOption α_1α_2} {bs : List α_1}, List.zipWithAll f [] bs = List.map (fun (b : α_1) => f none (some b)) bs
                                                                                                  @[simp]
                                                                                                  theorem List.zipWithAll_cons_cons :
                                                                                                  ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option αOption α_1α_2} {a : α} {as : List α} {b : α_1} {bs : List α_1}, List.zipWithAll f (a :: as) (b :: bs) = f (some a) (some b) :: List.zipWithAll f as bs
                                                                                                  def List.unzip {α : Type u} {β : Type v} :
                                                                                                  List (α × β)List α × List β

                                                                                                  O(|l|). Separates a list of pairs into two lists containing the first components and second components.

                                                                                                  • unzip [(x₁, y₁), (x₂, y₂), (x₃, y₃)] = ([x₁, x₂, x₃], [y₁, y₂, y₃])
                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    def List.range (n : Nat) :

                                                                                                    O(n). range n is the numbers from 0 to n exclusive, in increasing order.

                                                                                                    • range 5 = [0, 1, 2, 3, 4]
                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      Equations
                                                                                                      Instances For

                                                                                                        O(n). iota n is the numbers from 1 to n inclusive, in decreasing order.

                                                                                                        • iota 5 = [5, 4, 3, 2, 1]
                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          def List.iotaTR (n : Nat) :

                                                                                                          Tail-recursive version of iota.

                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            def List.enumFrom {α : Type u} :
                                                                                                            NatList αList (Nat × α)

                                                                                                            O(|l|). enumFrom n l is like enum but it allows you to specify the initial index.

                                                                                                            • enumFrom 5 [a, b, c] = [(5, a), (6, b), (7, c)]
                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              def List.enum {α : Type u} :
                                                                                                              List αList (Nat × α)

                                                                                                              O(|l|). enum l pairs up each element with its index in the list.

                                                                                                              • enum [a, b, c] = [(0, a), (1, b), (2, c)]
                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                def List.intersperse {α : Type u} (sep : α) :
                                                                                                                List αList α

                                                                                                                O(|l|). intersperse sep l alternates sep and the elements of l:

                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  def List.intercalate {α : Type u} (sep : List α) (xs : List (List α)) :
                                                                                                                  List α

                                                                                                                  O(|xs|). intercalate sep xs alternates sep and the elements of xs:

                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    @[inline]
                                                                                                                    def List.bind {α : Type u} {β : Type v} (a : List α) (b : αList β) :
                                                                                                                    List β

                                                                                                                    bind xs f is the bind operation of the list monad. It applies f to each element of xs to get a list of lists, and then concatenates them all together.

                                                                                                                    • [2, 3, 2].bind range = [0, 1, 0, 1, 2, 0, 1]
                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      @[inline]
                                                                                                                      def List.pure {α : Type u} (a : α) :
                                                                                                                      List α

                                                                                                                      pure x = [x] is the pure operation of the list monad.

                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        inductive List.lt {α : Type u} [LT α] :
                                                                                                                        List αList αProp

                                                                                                                        The lexicographic order on lists. [] < a::as, and a::as < b::bs if a < b or if a and b are equivalent and as < bs.

                                                                                                                        • nil: ∀ {α : Type u} [inst : LT α] (b : α) (bs : List α), List.lt [] (b :: bs)

                                                                                                                          [] is the smallest element in the order.

                                                                                                                        • head: ∀ {α : Type u} [inst : LT α] {a : α} (as : List α) {b : α} (bs : List α), a < bList.lt (a :: as) (b :: bs)

                                                                                                                          If a < b then a::as < b::bs.

                                                                                                                        • tail: ∀ {α : Type u} [inst : LT α] {a : α} {as : List α} {b : α} {bs : List α}, ¬a < b¬b < aList.lt as bsList.lt (a :: as) (b :: bs)

                                                                                                                          If a and b are equivalent and as < bs, then a::as < b::bs.

                                                                                                                        Instances For
                                                                                                                          instance List.instLTList {α : Type u} [LT α] :
                                                                                                                          LT (List α)
                                                                                                                          Equations
                                                                                                                          • List.instLTList = { lt := List.lt }
                                                                                                                          instance List.hasDecidableLt {α : Type u} [LT α] [h : DecidableRel fun (x x_1 : α) => x < x_1] (l₁ : List α) (l₂ : List α) :
                                                                                                                          Decidable (l₁ < l₂)
                                                                                                                          Equations
                                                                                                                          @[reducible]
                                                                                                                          def List.le {α : Type u} [LT α] (a : List α) (b : List α) :

                                                                                                                          The lexicographic order on lists.

                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            instance List.instLEList {α : Type u} [LT α] :
                                                                                                                            LE (List α)
                                                                                                                            Equations
                                                                                                                            • List.instLEList = { le := List.le }
                                                                                                                            instance List.instForAllListDecidableLeInstLEList {α : Type u} [LT α] [DecidableRel fun (x x_1 : α) => x < x_1] (l₁ : List α) (l₂ : List α) :
                                                                                                                            Decidable (l₁ l₂)
                                                                                                                            Equations
                                                                                                                            def List.isPrefixOf {α : Type u} [BEq α] :
                                                                                                                            List αList αBool

                                                                                                                            isPrefixOf l₁ l₂ returns true Iff l₁ is a prefix of l₂. That is, there exists a t such that l₂ == l₁ ++ t.

                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              def List.isPrefixOf? {α : Type u} [BEq α] :
                                                                                                                              List αList αOption (List α)

                                                                                                                              isPrefixOf? l₁ l₂ returns some t when l₂ == l₁ ++ t.

                                                                                                                              Equations
                                                                                                                              Instances For
                                                                                                                                def List.isSuffixOf {α : Type u} [BEq α] (l₁ : List α) (l₂ : List α) :

                                                                                                                                isSuffixOf l₁ l₂ returns true Iff l₁ is a suffix of l₂. That is, there exists a t such that l₂ == t ++ l₁.

                                                                                                                                Equations
                                                                                                                                Instances For
                                                                                                                                  def List.isSuffixOf? {α : Type u} [BEq α] (l₁ : List α) (l₂ : List α) :

                                                                                                                                  isSuffixOf? l₁ l₂ returns some t when l₂ == t ++ l₁.

                                                                                                                                  Equations
                                                                                                                                  Instances For
                                                                                                                                    @[specialize #[]]
                                                                                                                                    def List.isEqv {α : Type u} (as : List α) (bs : List α) (eqv : ααBool) :

                                                                                                                                    O(min |as| |bs|). Returns true if as and bs have the same length, and they are pairwise related by eqv.

                                                                                                                                    Equations
                                                                                                                                    Instances For
                                                                                                                                      def List.beq {α : Type u} [BEq α] :
                                                                                                                                      List αList αBool

                                                                                                                                      The equality relation on lists asserts that they have the same length and they are pairwise BEq.

                                                                                                                                      Equations
                                                                                                                                      Instances For
                                                                                                                                        instance List.instBEqList {α : Type u} [BEq α] :
                                                                                                                                        BEq (List α)
                                                                                                                                        Equations
                                                                                                                                        • List.instBEqList = { beq := List.beq }
                                                                                                                                        def List.replicate {α : Type u} (n : Nat) (a : α) :
                                                                                                                                        List α

                                                                                                                                        replicate n a is n copies of a:

                                                                                                                                        Equations
                                                                                                                                        Instances For
                                                                                                                                          def List.replicateTR {α : Type u} (n : Nat) (a : α) :
                                                                                                                                          List α

                                                                                                                                          Tail-recursive version of List.replicate.

                                                                                                                                          Equations
                                                                                                                                          Instances For
                                                                                                                                            def List.replicateTR.loop {α : Type u} (a : α) :
                                                                                                                                            NatList αList α
                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              def List.dropLast {α : Type u_1} :
                                                                                                                                              List αList α

                                                                                                                                              Removes the last element of the list.

                                                                                                                                              Equations
                                                                                                                                              Instances For
                                                                                                                                                @[simp]
                                                                                                                                                theorem List.length_replicate {α : Type u} (n : Nat) (a : α) :
                                                                                                                                                @[simp]
                                                                                                                                                theorem List.length_concat {α : Type u} (as : List α) (a : α) :
                                                                                                                                                @[simp]
                                                                                                                                                theorem List.length_set {α : Type u} (as : List α) (i : Nat) (a : α) :
                                                                                                                                                @[simp]
                                                                                                                                                theorem List.length_dropLast_cons {α : Type u} (a : α) (as : List α) :
                                                                                                                                                @[simp]
                                                                                                                                                theorem List.length_append {α : Type u} (as : List α) (bs : List α) :
                                                                                                                                                @[simp]
                                                                                                                                                theorem List.length_map {α : Type u} {β : Type v} (as : List α) (f : αβ) :
                                                                                                                                                @[simp]
                                                                                                                                                theorem List.length_reverse {α : Type u} (as : List α) :
                                                                                                                                                def List.maximum? {α : Type u} [Max α] :
                                                                                                                                                List αOption α

                                                                                                                                                Returns the largest element of the list, if it is not empty.

                                                                                                                                                Equations
                                                                                                                                                Instances For
                                                                                                                                                  def List.minimum? {α : Type u} [Min α] :
                                                                                                                                                  List αOption α

                                                                                                                                                  Returns the smallest element of the list, if it is not empty.

                                                                                                                                                  Equations
                                                                                                                                                  Instances For
                                                                                                                                                    @[inline]
                                                                                                                                                    def List.insert {α : Type u} [BEq α] (a : α) (l : List α) :
                                                                                                                                                    List α

                                                                                                                                                    Inserts an element into a list without duplication.

                                                                                                                                                    Equations
                                                                                                                                                    Instances For
                                                                                                                                                      instance List.decidableBEx {α : Type u} (p : αProp) [DecidablePred p] (l : List α) :
                                                                                                                                                      Decidable (∃ (x : α), x l p x)
                                                                                                                                                      Equations
                                                                                                                                                      instance List.decidableBAll {α : Type u} (p : αProp) [DecidablePred p] (l : List α) :
                                                                                                                                                      Decidable (∀ (x : α), x lp x)
                                                                                                                                                      Equations
                                                                                                                                                      Equations
                                                                                                                                                      • =
                                                                                                                                                      theorem List.of_concat_eq_concat {α : Type u} {as : List α} {bs : List α} {a : α} {b : α} (h : List.concat as a = List.concat bs b) :
                                                                                                                                                      as = bs a = b
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem List.concat_eq_append {α : Type u} (as : List α) (a : α) :
                                                                                                                                                      List.concat as a = as ++ [a]
                                                                                                                                                      theorem List.drop_eq_nil_of_le {α : Type u} {as : List α} {i : Nat} (h : List.length as i) :
                                                                                                                                                      List.drop i as = []